diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_tupleScript.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lem_tupleScript.sml | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_tupleScript.sml b/snapshots/hol4/lem/hol-lib/lem_tupleScript.sml new file mode 100644 index 00000000..7ee21f63 --- /dev/null +++ b/snapshots/hol4/lem/hol-lib/lem_tupleScript.sml @@ -0,0 +1,51 @@ +(*Generated by Lem from tuple.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_boolTheory lem_basic_classesTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "lem_tuple" + + + +(*open import Bool Basic_classes*) + +(* ----------------------- *) +(* fst *) +(* ----------------------- *) + +(*val fst : forall 'a 'b. 'a * 'b -> 'a*) +(*let fst (v1, v2)= v1*) + +(* ----------------------- *) +(* snd *) +(* ----------------------- *) + +(*val snd : forall 'a 'b. 'a * 'b -> 'b*) +(*let snd (v1, v2)= v2*) + + +(* ----------------------- *) +(* curry *) +(* ----------------------- *) + +(*val curry : forall 'a 'b 'c. ('a * 'b -> 'c) -> ('a -> 'b -> 'c)*) + +(* ----------------------- *) +(* uncurry *) +(* ----------------------- *) + +(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*) + + +(* ----------------------- *) +(* swap *) +(* ----------------------- *) + +(*val swap : forall 'a 'b. ('a * 'b) -> ('b * 'a)*) +(*let swap (v1, v2)= (v2, v1)*) + +val _ = export_theory() + |
