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