add_bare_numeral_form : (char * string option) -> unit

- STRUCTURE
- SYNOPSIS
- Adds support for annotated numerals to the parser/pretty-printer.
- LIBRARY
- Parse
- DESCRIPTION
- The function add_bare_numeral_form allows the user to give special meaning to strings of digits that are suffixed with single characters. A call to this function with pair argument (c, s) adds c as a possible suffix. Subsequently, if a sequence of digits is parsed, and it has the character c directly after the digits, then the natural number corresponding to these digits is made the argument of the “map function” corresponding to s.
This map function is computed as follows: if the s option value is NONE, then the function is considered to be the identity and never really appears; the digits denote a natural number. If the value of s is SOME s', then the parser translates the string to an application of s' to the natural number denoted by the digits.

- FAILURE
- Fails if the suffix character is not a letter.
- EXAMPLE
- The following function, binary_of, defined with equations:can be used to convert numbers whose decimal notation is x, to numbers whose binary notation is x (as long as x only involves zeroes and ones).
val bthm = |- binary_of n = if n = 0 then 0 else n MOD 10 + 2 * binary_of (n DIV 10) : thm

The following call to add_bare_numeral_form then sets up a numeral form that could be used by users wanting to deal with binary numbers:

- add_bare_numeral_form(#"b", SOME "binary_of"); > val it = () : unit - Term`1011b`; > val it = `1011b` : term - dest_comb it; > val it = (`binary_of`, `1011`) : term * term

- COMMENTS
- It is highly recommended that users avoid using suffixes that might be interpreted as hexadecimal digits A to F, in either upper or lower case. Further, HOL convention has it that suffix character should be lower case.
- USES
- If one has a range of values that are usefully indexed by natural numbers, the function add_bare_numeral_form provides a syntactically convenient way of reading and writing these values. If there are other functions in the range type such that the mapping function is a homomorphism from the natural numbers, then add_numeral_form could be used, and the appropriate operators (+, * etc) overloaded.
- SEEALSO

HOL Kananaskis-14