Lem_set_helpers.thy

chapter {* Generated by Lem from set_helpers.lem. *}

theory "Lem_set_helpers" 

imports 
 	 Main
	 "Lem_bool" 
	 "Lem_basic_classes" 
	 "Lem_maybe" 
	 "Lem_function" 
	 "Lem_num" 

begin 

(******************************************************************************)
(* Helper functions for sets                                                  *)
(******************************************************************************)

(* Usually there is a something.lem file containing the main definitions and a 
   something_extra.lem one containing functions that might cause problems for
   some backends or are just seldomly used.

   For sets the situation is different. folding is not well defined, since it
   is only sensibly defined for finite sets and the traversal 
   order is underspecified. *) 

(* ========================================================================== *)
(* Header                                                                     *)
(* ========================================================================== *)

(*open import Bool Basic_classes Maybe Function Num*) 

(*open import {coq} `Coq.Lists.List`*)

(* ------------------------ *)
(* fold                     *)
(* ------------------------ *)

(* fold is suspicious, because if given a function, for which
   the order, in which the arguments are given, matters, its
   results are undefined. On the other hand, it is very handy to
   define other - non suspicious functions. 

   Moreover, fold is central for OCaml, since it is used to
   compile set comprehensions *)

(*val fold : forall 'a 'b. ('a -> 'b -> 'b) -> set 'a -> 'b -> 'b*)


end