summaryrefslogtreecommitdiff
path: root/snapshots/hol4/lem/hol-lib/lem_tupleScript.sml
diff options
context:
space:
mode:
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_tupleScript.sml')
-rw-r--r--snapshots/hol4/lem/hol-lib/lem_tupleScript.sml51
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()
+