%block
From The Twelf Project
A %block declaration names a block, which is a partial description of an LF context. Blocks are composed into regular worlds with %worlds declarations, which describe the complete set of possible contexts for a type family. This description of the context is an important part of the adequacy of the metatheorem established by a %total declaration.
A %block declaration acts more like a definition than other keywords, which generally cause Twelf to do something rather than define something. The obvious exception to this is %define.
[edit] Sample %block declarations
These sample %block declarations are in the context of the definitions of exp and height in the %worlds article.
Using this block in a %worlds declaration means that arbitrary variables representing expressions can appear in the context:
%block var-rand : block {x : exp}.
Using this block in a %worlds declaration means that variables representing expressions can appear in the context, but only if they are accompanied by a judgment that defines the height of that variable to be one.
%block var-height : block {x : exp}{_ : height x (s z)}.
Using this block in a %worlds declaration means that variables representing expressions can appear in the context, but only if they are accompanied by a judgment that defines the height of that variable to be some natural number.
%block var-heightN : some {N: nat} block {x : exp}{_ : height x N}.
[edit] See also
- %worlds
- Proving totality assertions in non-empty contexts in the tutorial Proving metatheorems with Twelf
- Totality assertion
- Regular Worlds in the User's Guide
