The Twelf Project:Literate Twelf

From The Twelf Project
Jump to: navigation, search

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.

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.


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


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.