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