blob: 403564484745e1611817be11e80d5a2cedd17573 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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 -> natural*)
(*val integerOfString : string -> integer*)
(* Truncation integer division (round toward zero) *)
(*val integerDiv_t: integer -> integer -> integer*)
(* Truncation modulo *)
(*val integerRem_t: integer -> integer -> integer*)
(* Flooring modulo *)
(*val integerRem_f: integer -> integer -> integer*)
val _ = export_theory()
|
