summaryrefslogtreecommitdiff
path: root/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml
diff options
context:
space:
mode:
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml')
-rw-r--r--snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml34
1 files changed, 34 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml
new file mode 100644
index 00000000..69644f94
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml
@@ -0,0 +1,34 @@
+(*Generated by Lem from num_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_numTheory lem_stringTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_num_extra"
+
+(* **************************************************** *)
+(* *)
+(* A library of additional functions on numbers *)
+(* *)
+(* **************************************************** *)
+
+(*open import Num*)
+(*open import String*)
+
+(*val naturalOfString : string -> Num.natural*)
+
+(*val integerOfString : string -> Num.integer*)
+
+
+(* Truncation integer division (round toward zero) *)
+(*val integerDiv_t: Num.integer -> Num.integer -> Num.integer*)
+
+(* Truncation modulo *)
+(*val integerRem_t: Num.integer -> Num.integer -> Num.integer*)
+
+(* Flooring modulo *)
+(*val integerRem_f: Num.integer -> Num.integer -> Num.integer*)
+val _ = export_theory()
+