7.12.8 Definition macros

Page 238 of 800

Search internet

The base and check pages define a number of macros which make it easier to state various definitions:

The definitions read:

macro define value define x as y end define as define value of root protect x end protect as y end define end define

macro define message define x as y end define as define message of root protect x end protect as y end define end define

macro define tex show define x as y end define as Define tex show of root protect x end protect as y end define end define

macro define tex use define x as y end define as Define tex use of root protect x end protect as y end define end define

macro define destructure define x as y end define as define destructure of root protect x end protect as y end define end define

macro define statement define x as y end define as define statement of x as y end define end define

macro define proof define x as y end define as define proof of x as y end define end define

macro define meta define x as y end define as define meta of x as y end define end define

macro define math define x as y end define as define math of x as y end define end define

macro define tactic define x as y end define as define tactic of x as y end define end define

macro define unitac define x as y end define as define unitac of x as y end define end define

macro define locate define x as y end define as define locate of root protect x end protect as y end define end define

The exclamation mark in use and show definitions indicates that y should be rendered using 'show' rendering. That is important since the right hand side of use and show definitions contain lots of TeX codes which have to be escaped when rendering the use and show definitions. At present, this has no uses, but users who decide to render extracts of pages in PDF will need it.

Macros for defining the four functions which are directly invoked by lgc(1) and which are under author control read:

macro define verifier x end verifier as define claim of self as x end define end define

macro define unpacker x end unpacker as define unpack of self as x end define end define

macro define renderer x end renderer as define render of self as x end define end define

macro define expander x end expander as define macro of self as x end define end define

The lgs source of the constructs reads:

value define x as y end define
message define x as y end define
tex show define x as y end define
tex use define x as y end define
destructure define x as y end define
statement define x as y end define
proof define x as y end define
meta define x as y end define
math define x as y end define
tactic define x as y end define
unitac define x as y end define
locate define x as y end define
verifier x end verifier
unpacker x end unpacker
renderer x end renderer
expander x end expander

Page 238 of 800

Search logiweb.eu