diff options
| author | dos-reis <gdr@axiomatics.org> | 2010-06-29 21:31:12 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2010-06-29 21:31:12 +0000 |
| commit | 3f4d38826d28da40a6509a9afc37b8cbaebd080e (patch) | |
| tree | 7cda4231bb62a4469d5fed7dd88c34f91a62ed09 /src/algebra/mkrecord.spad.pamphlet | |
| parent | 2394bfc186f7b57a7b8b737b4b17e1140d756416 (diff) | |
| download | open-axiom-3f4d38826d28da40a6509a9afc37b8cbaebd080e.tar.gz | |
* algebra/indexedp.spad.pamphlet (IndexedDirectProductObject)
[indexedDirectProductObject]: New.
(IndexedDirectProductAbelianMonoid): Rework implementation.
[construct]: Likewise.
Diffstat (limited to 'src/algebra/mkrecord.spad.pamphlet')
| -rw-r--r-- | src/algebra/mkrecord.spad.pamphlet | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/algebra/mkrecord.spad.pamphlet b/src/algebra/mkrecord.spad.pamphlet index ea6e3795..0b0bc331 100644 --- a/src/algebra/mkrecord.spad.pamphlet +++ b/src/algebra/mkrecord.spad.pamphlet @@ -42,12 +42,11 @@ import SetCategory ++ Description: This domain provides a very simple representation ++ of the notion of `pair of objects'. It does not try to achieve ++ all possible imaginable things. -Pair(S: Type, T: Type): Public == Private where - Public ==> Type with +Pair(S: Type,T: Type): Public == Private where + Public == Type with if S has CoercibleTo OutputForm and T has CoercibleTo OutputForm then CoercibleTo OutputForm - if S has SetCategory and T has SetCategory then SetCategory pair: (S,T) -> % @@ -59,20 +58,20 @@ Pair(S: Type, T: Type): Public == Private where second: % -> T ++ second(p) extracts the second components of `p'. - Private ==> add - Rep := Record(fst: S, snd: T) + Private == add + Rep == Record(fst: S, snd: T) pair(s,t) == - [s,t]$Rep + per [s,t]$Rep construct(s,t) == pair(s,t) first x == - x.fst + rep(x).fst second x == - x.snd + rep(x).snd if S has CoercibleTo OutputForm and T has CoercibleTo OutputForm then coerce x == @@ -81,6 +80,7 @@ Pair(S: Type, T: Type): Public == Private where if S has SetCategory and T has SetCategory then x = y == first(x) = first(y) and second(x) = second(y) + @ |