diff options
Diffstat (limited to 'theories/FSets/FMapInterface.v')
| -rw-r--r-- | theories/FSets/FMapInterface.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index a6f90acb7..01362936c 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -43,7 +43,7 @@ Unset Strict Implicit. - no [iter] function, useless since Coq is purely functional - [option] types are used instead of [Not_found] exceptions - - more functions are provided: [elements] and [map2] + - more functions are provided: [elements] and [cardinal] and [map2] *) @@ -116,6 +116,9 @@ Module Type WSfun (E : EqualityType). (** [elements m] returns an assoc list corresponding to the bindings of [m], in any order. *) + Parameter cardinal : t elt -> nat. + (** [cardinal m] returns the number of bindings in [m]. *) + Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A. (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], where [k1] ... [kN] are the keys of all bindings in [m] @@ -181,6 +184,9 @@ Module Type WSfun (E : EqualityType). property that is really weaker: *) Parameter elements_3w : NoDupA eq_key (elements m). + (** Specification of [cardinal] *) + Parameter cardinal_1 : cardinal m = length (elements m). + (** Specification of [fold] *) Parameter fold_1 : forall (A : Type) (i : A) (f : key -> elt -> A -> A), |