Parse.set_known

STRUCTURE

SYNOPSIS

Specifies the list of names that should be parsed as constants.

LIBRARY

Parse

DESCRIPTION

One of the final phases of parsing is the resolution of free names in putative terms as either variables, constants or overloaded constants. If such a free name is not overloaded, then the list of known constants is consulted to determine whether or not to treat it as a constant. If the name is not present in the list, then it will be treated as a free variable.

FAILURE

Never fails. If a name is specified in the list of constants that is not in fact a constant, a warning message is printed, and that name is ignored.

EXAMPLE

- known_constants();
> val it =
    ["bool_case", "ARB", "TYPE_DEFINITION", "ONTO", "ONE_ONE", "COND",
     "LET", "?!", "~", "F", "\\/", "/\\", "!", "T", "?", "@",
     "==>", "="]
    : string list
- Term`p /\ q`;
> val it = `p /\ q` : term
- set_known_constants (Lib.subtract (known_constants()) ["/\\"]);
> val it = () : unit
- Term`p /\ q`;
<<HOL message: inventing new type variable names: 'a, 'b, 'c.>>
> val it = `p /\ q` : term
- strip_comb it;
> val it = (`$/\`, [`p`, `q`]) : term * term list
- dest_var (#1 it);
> val it = ("/\\", `:'a -> 'b -> 'c`) : string * hol_type

USES

When writing library code that calls the parser, it can be useful to know exactly what constants the parser will "recognise".

COMMENTS

This function does not affect the contents of a theory. A constant made invisible using this call is still really present in the theory; it is just harder to find.

SEEALSO

hidden, hide, known_constants, reveal