term_grammar.clear

STRUCTURE

SYNOPSIS

Remove non-trivial overloading from a term grammar

DESCRIPTION

For a term grammar tmG, clear_overloads tmG is the similar grammar, changed to remove non-trivial overloading. (Each constant remains overloaded with itself, which avoids the printing of the theory name for every constant).

USES

Sometimes overloading can be too helpful, when we would like to see the structure of a term (eg, in finding which theorems could simplify it).

EXAMPLE

In this example we obtain the current type and term grammars tyG and tmG, then reset the current grammars to be these, except with overloading cleared from the term grammar. We print some theorems (eg, to view their internal structure), and finally we reset the current grammars to the original ones.

> ratTheory.RATND_RAT_OF_NUM;
val it = |- (RATN (&n) = &n) /\ (RATD (&n) = 1): thm
> rich_listTheory.MEM_TAKE;
val it = |- !m l. m <= LENGTH l ==> !x. MEM x (TAKE m l) ==> MEM x l: thm

val (tyG, tmG) = Parse.current_grammars () ;
Parse.temp_set_grammars (tyG, term_grammar.clear_overloads tmG) ;

> ratTheory.RATND_RAT_OF_NUM;
val it = |- (RATN (rat_of_num n) = int_of_num n) /\ 
  (RATD (rat_of_num n) = 1n): thm
> rich_listTheory.MEM_TAKE;
val it = |- !m l.  m <= LENGTH l ==>
  !x. x IN LIST_TO_SET (TAKE m l) ==> x IN LIST_TO_SET l: thm

Parse.temp_set_grammars (tyG, tmG) ;

COMMENTS

To print just a few terms without overloading, print_without_macros may be easier.

SEEALSO

print_without_macros, current_grammars, temp_set_grammars