Skip to content
STELF
Documentation out of dateLearn more

%block

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 STELF to do something rather than define something. The obvious exception to this is %define.

Sample %block declarations

Section titled “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 {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 {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 [N nat] {x exp} {_ height x N}%.

Block definitions

Section titled “Block definitions”

Block definitions allow multiple blocks to be combined:

%sort typ %.
%sort exp {_ typ} %.
%block typ-var {a typ}%.
%block exp-var [T typ] {x exp T}%.
%block vars%.

Using vars in a %worlds declaration is the same as using typ-var | exp-var, and in fact when STELF prints out the %worlds declaration, block definitions will be automatically expanded.

%worlds (vars) (exp _) %.

See also

Section titled “See also”