Merge branch 'sail2' into mappings

1 files changed, 47 insertions, 0 deletions

diff --git a/snapshots/hol4/lem/hol-lib/lem_set_helpersScript.sml b/snapshots/hol4/lem/hol-lib/lem_set_helpersScript.sml
new file mode 100644
index 00000000..5ce9f938
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_set_helpersScript.sml
@@ -0,0 +1,47 @@
+(*Generated by Lem from set_helpers.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_functionTheory lem_numTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_set_helpers"
+
+(******************************************************************************)
+(* 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*)
+
+
+val _ = export_theory()
+