blob: 0611862e454c3647bf45d9655a93e1110c972e4a (
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
|
chapter \<open>Generated by Lem from num_extra.lem.\<close>
theory "Lem_num_extra"
imports
Main
"Lem_num"
"Lem_string"
begin
(* **************************************************** *)
(* *)
(* 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*)
end
|
