Define declaration

From The Twelf Project
Jump to: navigation, search

The name of this article should be %define. There's a quirk of Unicode that causes this to not behave correctly.

The %define declaration allows the outputs of a successful %solve declaration to be bound to a name which can be used later on in the context.


Given a standard declaration of natural numbers and plus with a few constants defined:

nat : type.

z : nat. 
s : nat -> nat.

n0 = z.
n1 = s n0. 
n2 = s n1. 
n3 = s n2. 
n4 = s n3. 

plus : nat -> nat -> nat -> type.
%mode plus +N1 +N2 -N3.

plus/z : plus z N N.

plus/s : plus (s N1) N2 (s N3) 
          <- plus N1 N2 N3.

We can use %define to define the natural number representing 7 by adding three and four. Note that we don't care about the proof witness in this particular case, just the output of the relation, so we put an underscore instead of an identifier to the left of the colon:

%define n7 = N
%solve _ : plus n4 n3 N.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on

%solve plus n4 n3 N. OK n7 : nat = s (s (s (s n3))). _ : plus n4 n3 (s (s (s (s n3)))) = plus/s (plus/s (plus/s (plus/s plus/z))).

%% OK %%

See also