8.4.7 Local definitions

Prev Up Next Page 322 of 800 Search internet

The following construct allows to make a local definition:

   line L : Local >> C = D ; N

The construct locally defines C to macro expand to D inside N. As an example, if one writes

   line L01 : Local >> x = 0 ; ...

then one can use x as shorthand for 0 inside the remainder of the proof.

The purpose of the construct is to enhance human readability of proofs.

Local macros are expanded during macro expansion. Error messages from the proof checker are generated after macro expansion. Thus, if one locally defines x to be 0 and then makes an error involving x, then one should be prepared to see 0 rather than x in the associated error message.

Local definitions can be used both in T proofs and plain proofs.

Prev Up Next Page 322 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05