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 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.
