blob: c1edb1947ae1a14d46428fd606652650529567a5 (
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 \<open>num_extra.lem\<close>.\<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
|
