From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

The TwelfTag system is a way of adding Twelf code directly into the Twelf Project Wiki. This page gives an introduction to TwelfTag for readers. The page Project:TwelfTag has information about TwelfTag for editors, and the Twelf Live system provides a more interactive way of using Twelf with on this website.

Syntax highlighting

The most basic function of TwelfTag is to highlight Twelf code much the same way that Emacs does. Names are red, and metavariables (free variables) are in blue.

elem : type.

list : type.
nil : list.
cons : elem -> list -> list.

list-reverse : list -> list -> list -> type.
lr/nil : list-reverse nil L L.
lr/cons : list-reverse (cons E L1) L2 L3
           <- list-reverse L1 (cons E L2) L3.

Showing Twelf's response

When Twelf checks a piece of code, it produces some output that represents Twelf's reconstruction of that code and a message (%% OK %% or %% ABORT %%) that signals whether it was successful. Sometimes it is helpful to show Twelf's response in an article, and TwelfTag can do this too, showing Twelf's response in green.

%solve test : {e1}{e2}{e3}{e4} list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil _.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on

%solve {e1:elem} {e2:elem} {e3:elem} {e4:elem} list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil (X1 e1 e2 e3 e4). OK test : {e1:elem} {e2:elem} {e3:elem} {e4:elem} list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil (cons e4 (cons e2 (cons e3 (cons e1 nil)))) = [e1:elem] [e2:elem] [e3:elem] [e4:elem] lr/cons (lr/cons (lr/cons (lr/cons lr/nil))).

%% OK %%

Linking to Twelf code and Twelf output

TwelfTag has the ability to link, inside a page, to the code that has been shown highlighted on that page, and also to link to the response Twelf gives when checking that code.

  • This link shows you the twelf code (the code that is shown with syntax ) for this page.
  • This link shows you Twelf's response from reading the code on this page.

"Literate Twelf"

For some pages, including this one, the page itself is written in valid Twelf that is then automatically transformed into an article. Pages written in this way look exactly like other pages, but they have a note at the top of the article that reports on Twelf's status after reading the file - %% OK %% means everything checked out, and %% ABORT %% means that there was a problem - and links to both the code and Twelf's response. More information on writing articles with this feature can be found at the page on Literate Twelf.