%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] Block definitions
As of 1.7.1, block definitions are now supported.
typ : type. exp : typ -> type. %block typ-var : block {a : typ}. %block exp-var : some {T : typ} block {x : exp T}. %block vars = (typ-var | exp-var).
Using vars in a %worlds declaration is the same as using typ-var | exp-var, and in fact when Twelf prints out the %worlds declaration, block definitions will be automatically expanded.
%worlds (vars) (exp _).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)%worlds (typ-var | exp-var) (exp _).
%% OK %%
[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
