|
From: | Ralf Hemmecke |
Subject: | Re: [Axiom-developer] Unions in Spad |
Date: | Fri, 13 Jul 2007 08:26:01 +0200 |
User-agent: | Thunderbird 2.0.0.4 (X11/20070604) |
=--- 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
[Prev in Thread] | Current Thread | [Next in Thread] |