forked from HOL-Theorem-Prover/HOL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmlibArbint.sig
45 lines (34 loc) · 958 Bytes
/
mlibArbint.sig
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
35
36
37
38
39
40
41
42
43
44
45
(* Copyright (c) Michael Norrish *)
signature mlibArbint =
sig
eqtype int
type num = mlibArbnum.num
val zero : int
val one : int
val two : int
val toString : int -> string
val fromString : string -> int
val fromInt : Int.int -> int
val fromNat : num -> int
val toInt : int -> Int.int
val toNat : int -> num
val + : (int * int) -> int
val - : (int * int) -> int
val * : (int * int) -> int
val div : (int * int) -> int
val mod : (int * int) -> int
val quot : (int * int) -> int
val rem : (int * int) -> int
val divmod : (int * int) -> (int * int)
val quotrem: (int * int) -> (int * int)
val negate : int -> int
val ~ : int -> int
val < : int * int -> bool
val <= : int * int -> bool
val > : int * int -> bool
val >= : int * int -> bool
val abs : int -> int
val compare : int * int -> order
val min : int * int -> int
val max : int * int -> int
end