Syntax (Object logic)
From The Twelf Project
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.
- Read the introductions to Twelf to learn how to represent syntax in LF.
- Judgments as types
- Higher-order abstract syntax
This page is incomplete. We should expand it.