diff options
Diffstat (limited to 'src/algebra')
| -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) + @ |