Structure base_tokens
signature base_tokens =
sig
exception LEX_ERR of string * locn.locn
type fracinfo = {wholepart: Arbnum.num, fracpart: Arbnum.num, places : int}
datatype 'a base_token =
BT_Ident of string
| BT_Numeral of (Arbnum.num * char option)
| BT_DecimalFraction of fracinfo
| BT_AQ of 'a
| BT_EOI
val toString : 'a base_token -> string
val allow_octal_input : bool ref
val preferred_output_base : StringCvt.radix ref
val parse_numeric_literal : string * locn.locn -> Arbnum.num * char option
val parse_fraction : string * locn.locn -> fracinfo
end
HOL 4, Kananaskis-10