1signature ratSyntax =
2sig
3  type term = Term.term
4  type hol_type = Abbrev.hol_type
5
6  val rat : hol_type
7
8  val rat_0_tm    : term
9  val rat_1_tm    : term
10  val is_literal  : term -> bool
11
12  val rat_nmr_tm  : term
13  val rat_dnm_tm  : term
14  val rat_sgn_tm  : term
15  val rat_of_num_tm : term
16
17  val rat_ainv_tm : term
18  val rat_minv_tm : term
19
20  val rat_add_tm  : term
21  val rat_sub_tm  : term
22  val rat_mul_tm  : term
23  val rat_div_tm  : term
24
25  val rat_les_tm  : term
26  val rat_gre_tm  : term
27  val rat_leq_tm  : term
28  val rat_geq_tm  : term
29
30  val mk_rat_nmr  : term -> term
31  val mk_rat_dnm  : term -> term
32  val mk_rat_sgn  : term -> term
33  val mk_rat_of_num : term -> term
34
35  val mk_rat_ainv : term -> term
36  val mk_rat_minv : term -> term
37
38  val mk_rat_add  : term * term -> term
39  val mk_rat_sub  : term * term -> term
40  val mk_rat_mul  : term * term -> term
41  val mk_rat_div  : term * term -> term
42
43  val dest_rat_nmr        : term -> term
44  val dest_rat_dnm        : term -> term
45  val dest_rat_sgn        : term -> term
46  val dest_rat_of_num : term -> term
47
48  val dest_rat_ainv       : term -> term
49  val dest_rat_minv       : term -> term
50
51  val dest_rat_add        : term -> term * term
52  val dest_rat_sub        : term -> term * term
53  val dest_rat_mul        : term -> term * term
54  val dest_rat_div        : term -> term * term
55
56  val dest_rat_les        : term -> term * term
57  val dest_rat_gre        : term -> term * term
58  val dest_rat_leq        : term -> term * term
59  val dest_rat_geq        : term -> term * term
60
61  val is_rat_nmr  : term -> bool
62  val is_rat_dnm  : term -> bool
63  val is_rat_sgn  : term -> bool
64  val is_rat_of_num : term -> bool
65
66  val is_rat_ainv : term -> bool
67  val is_rat_minv : term -> bool
68
69  val is_rat_add  : term -> bool
70  val is_rat_sub  : term -> bool
71  val is_rat_mul  : term -> bool
72  val is_rat_div  : term -> bool
73
74  val is_rat_les  : term -> bool
75  val is_rat_gre  : term -> bool
76  val is_rat_leq  : term -> bool
77  val is_rat_geq  : term -> bool
78
79  val list_rat_add : term list -> term
80  val list_rat_mul : term list -> term
81
82  val strip_rat_add : term -> term list
83  val strip_rat_mul : term -> term list
84
85  val int_of_term : term -> Arbint.int (* partial! *)
86  val term_of_int : Arbint.int -> term
87
88end
89