%block

From The Twelf Project
Jump to: navigation, search

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.


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}.

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+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%worlds (typ-var | exp-var) (exp _).

%% OK %%

See also