Page 322 of 800
| 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.
| Page 322 of 800 | Search logiweb.eu |