=--- 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
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
