The Twelf Project:Literate Twelf/Sample Page
From The Twelf Project
| This is Literate Twelf Code: here Status: %% OK %% Output: here. |
Some natural numbers; a demo of Literate Twelf.
Contents |
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 (built 03/19/11 at 09:41:05 on gs6177)%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.
