1signature Literal = 2sig 3 type term = HolKernel.term 4 type num = Arbnum.num 5 6 val is_zero : term -> bool 7 val is_numeral : term -> bool 8 val dest_numeral : term -> Arbnum.num 9 val gen_mk_numeral : {mk_comb : 'a * 'a -> 'a, 10 ZERO : 'a, 11 ALT_ZERO: 'a, 12 NUMERAL : 'a, 13 BIT1 : 'a, 14 BIT2 : 'a} -> Arbnum.num -> 'a 15 16 val is_emptystring : term -> bool 17 val is_string_lit : term -> bool 18 val dest_string_lit : term -> String.string 19 val mk_string_lit : {mk_string : 'a * 'a -> 'a, 20 emptystring : 'a, 21 fromMLchar : char -> 'a} -> String.string -> 'a 22 val string_literalpp: string -> string 23 24 val is_char_lit : term -> bool 25 val dest_char_lit : term -> Char.char 26 27 val is_literal : term -> bool 28 val is_pure_literal : term -> bool 29 val add_literal : (term -> bool) -> unit 30 31 val relaxed_dest_numeral : term -> Arbnum.num 32 val relaxed_dest_string_lit : term -> String.string 33end 34