diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml | 34 |
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() + |
