Re: [Axiom-developer] Unions in Spad

[Ralf Hemmecke]

=--- union-test.spad ----
> )abbrev domain BAR Bar
>
> Bar() : Exp == Impl where
>    Exp == with
>      inj : Integer -> %
>      inj : String -> %
>      prj : % -> Integer
>    Impl == add
>      Rep := Union(tag1: Integer, tag1: String)
>      inj (n : Integer) : % == [n]
>      inj (s : String) : % == [s]
>      prj p == (p::Rep).tag1

Stephen, have you ever thought about the difference between Rep and %?
The type of [n] would be Rep, since there is no function

  bracket: Integer -> %

so if you write

  inj (n : Integer) : % == [n]

as above, that should be a type error.

Ralf