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.

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.

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.