The Twelf Project:Literate Twelf
From The Twelf Project
The Literate Twelf extension is a relatively simple modification of TwelfTag intended to facilitate both offline editing, as well as direct use, of pages on this wiki. Literate Twelf pages interperet text inside of multi-line comments as are automatically run through Twelf by the Literate Twelf extension, and Twelf's output ("%% OK %%" or "%% ABORT %%") is displayed in a box at the top of the page.
[edit] Using Literate Twelf
If a file on the wiki starts with the string %{, a preprocesser is invoked that (essentially) turns all instances of %{ to </twelf> and all instances of }% into <twelf>, transforming the Twelf file with comments into a Mediawiki file with escaped TwelfTag sequences.
Furthermore, if a pipe characther | appears on the same line as the }% symbol, the text between the | and the }% will be interpreted as options to the <twelf> tag.
[edit] Limitations
- Multi-line comments cannot be nested within a Literate Twelf file.
- Section editing is disabled for Literate Twelf files on the wiki, as this could potentially lead to unpredictable results.
[edit] Demo
The following Literate Twelf page is demonstrated here. Notice that because a | appears on the second line, the comment cannot be closed on that line or the entire segment Literate Twelf]]. would be interpreted as TwelfTag options.
%{
Some natural numbers; a demo of [[Project:Literate Twelf|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: |check=decl}%
%solve _ : plus (s (s (s z))) (s (s z)) N.
%.
This is a pretty boring presentation of the natural numbers;
it is roughly like all the other ones, like the article on [[natural numbers]].
