Syntax (Object logic)

From The Twelf Project
Jump to: navigation, search

The syntax of an object logic is commonly encoded as an LF type family of kind type.

For example, if the language of our object logic is the natural numbers, its syntax would be declared in the following way.

% declare a type family of kind "type" for natural numbers.
nat : type.

% inhabit the nat with the appropriate constructors.

nat/z : nat.
nat/s : nat -> nat.

See also

This page is incomplete. We should expand it.