The Twelf Project:Literate Twelf/Sample Page

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Some natural numbers; a demo of Literate Twelf.

Syntax

nat: type.
z : nat.
s : nat -> nat.

Judgments

Equality

id-nat : nat -> nat -> type.
id-nat/refl : id-nat N N.

Addition

plus : nat -> nat -> nat -> type.
plus/z : plus z N N.
plus/s : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

Now we can see what it looks like to run a query:

%solve _ : plus (s (s (s z))) (s (s z)) N.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve plus (s (s (s z))) (s (s z)) N. OK _ : plus (s (s (s z))) (s (s z)) (s (s (s (s (s z))))) = plus/s (plus/s (plus/s plus/z)).

%% OK %%

This is a pretty boring presentation of the natural numbers; it is roughly like all the other ones, like the article on natural numbers.