diff options
| author | dos-reis <gdr@axiomatics.org> | 2013-05-17 10:50:09 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2013-05-17 10:50:09 +0000 |
| commit | fd52eb1ee7ab42be1fdc73d9fc91d79abd0abd25 (patch) | |
| tree | 8826031bbc15074f25d2d3c50b2696f494d7868f /src/algebra/aggcat.spad.pamphlet | |
| parent | 1e6db8d4424e63a8992d7fc04917ddfd6ce94378 (diff) | |
| download | open-axiom-fd52eb1ee7ab42be1fdc73d9fc91d79abd0abd25.tar.gz | |
* algebra/aggcat.spad.pamphlet (FiniteAggregate): More defaults.
(Aggregate): Remove default implementation of empty?
Diffstat (limited to 'src/algebra/aggcat.spad.pamphlet')
| -rw-r--r-- | src/algebra/aggcat.spad.pamphlet | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/algebra/aggcat.spad.pamphlet b/src/algebra/aggcat.spad.pamphlet index ebbf2f97..2d539d44 100644 --- a/src/algebra/aggcat.spad.pamphlet +++ b/src/algebra/aggcat.spad.pamphlet @@ -56,8 +56,6 @@ Aggregate: Category == Type with add eq?(a,b) == %peq(a,b)$Foreign(Builtin) sample() == empty() - if % has finiteAggregate then - empty? a == #a = 0 @ @@ -199,6 +197,14 @@ FiniteAggregate(S: Type): Category == Exports where ++ \axiom{member?(x,u) = reduce(or,[x=y for y in u],false)}. add empty? x == #x = 0 + #x == # members x + any?(f, x) == or/[f e for e in members x] + every?(f, x) == and/[f e for e in members x] + count(f:S -> Boolean, x:%) == +/[1 for e in parts x | f e] + if S has BasicType then + count(s:S, x:%) == count(s = #1, x) + member?(e, x) == any?(e = #1,x) + @ |