Page 323 of 800
| Page 323 of 800 | Search internet |
The following construct allows to group a sequence of proof lines into a block:
line L1 : Block >> Begin ; B line L2 : Block >> End ; N
The construct above is used for expressing Line L02 and L08 of the multzero proof:
In the example above, Line L03-L07 constitute the body B of the block and Line L09-L10 constitute the 'next' argument N of the block.
The block construct generates two lines (Line L02 and Line L08 in the example above). Both lines have a line number. The first of the two line numbers (L02 in the example above) is purely decorative.
Blocks can be used both in T proofs and plain proofs. After a block you can refer to the end line of the block but not to any line inside the block.
Blocks can be nested. The 'use' rendering aspect of blocks does indentation.
| Page 323 of 800 | Search logiweb.eu |