Abbrev declaration

From The Twelf Project
Jump to: navigation, search

The %abbrev keyword can be placed before any definition in a Twelf signature to cause the definition to, in the future, act as syntatic shorthand for some other term.


Say, for some reason, we had extremely verbose names for the syntax of the natural numbers.

this-is-a-long-name-for-nat : type.
this-is-a-long-name-for-z : this-is-a-long-name-for-nat.
this-is-a-long-name-for-s : this-is-a-long-name-for-nat -> this-is-a-long-name-for-nat.

We can define nat and z from their long names using %abbrev, and s without %abbrev.

%abbrev nat = this-is-a-long-name-for-nat.
%abbrev z   = this-is-a-long-name-for-z.
s   = this-is-a-long-name-for-s.

We can see the difference here - while definitions like s will be expanded only if they have to be, definitions made with the %abbrev keyword are always expanded by Twelf.

three = s (s (s z)).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on

three : this-is-a-long-name-for-nat = s (s (s this-is-a-long-name-for-z)).

%% OK %%

See also