From fd52eb1ee7ab42be1fdc73d9fc91d79abd0abd25 Mon Sep 17 00:00:00 2001
From: dos-reis <gdr@axiomatics.org>
Date: Fri, 17 May 2013 10:50:09 +0000
Subject: 	* algebra/aggcat.spad.pamphlet (FiniteAggregate): More
 defaults. 	(Aggregate): Remove default implementation of empty?

---
 src/algebra/aggcat.spad.pamphlet | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/algebra/aggcat.spad.pamphlet')

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)
+      
 
 @
 
-- 
cgit v1.2.3