Abbrev declaration
From The Twelf Project
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.
[edit] Example
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 (built 03/19/11 at 09:41:05 on gs6177)three : this-is-a-long-name-for-nat = s (s (s this-is-a-long-name-for-z)).
%% OK %%
[edit] See also
- Definitions in the User's Guide
