example Twelf code

nat.elf

% in reply to http://www.reddit.com/r/haskell/comments/23cajh/how_can_i_avoid_this_function_to_typecheck/

% the datatype nat, with constructors z and s.
nat : type.
z : nat.
s : nat -> nat.

% a bunch of synonyms
zero  = z               : nat.
one   = s z             : nat.
two   = s (s z)         : nat.
three = s (s (s z))     : nat.
four  = s (s (s (s z))) : nat.

% the function is-nat, which maps any nat to itself.
% like all Twelf functions, it is really a relation:
% z is related to itself, and (s A) is related to (s R) iff A is related to R.
is-nat : nat -> nat -> type.
is-nat/z : is-nat z z.
is-nat/s : is-nat (s A) (s R)
        <- is-nat A R.

% to call the function is-nat on the input two, we ask the solver to find
% an R such that two is related to R via is-nat.
%solve _ : is-nat two R.
% => _ : is-nat two (s (s z))
%      = is-nat/s (is-nat/s is-nat/z).
% 
% note that the solver found both a value for R and a proof (is-nat/s (is-nat/s is-nat/z))
% that two is related to that R.

% is-even maps even nats to themselves, and is undefined for odd nats.
is-even : nat -> nat -> type.
is-even/z : is-even z z.
is-even/ss : is-even (s (s A)) (s (s R))
          <- is-even A R.

%solve _ : is-even two R.
% => _ : is-even two (s (s z))
%      = is-even/ss is-even/z.

% of course, the solver cannot find a solution if there isn't one.
%   %solve _ : is-even (s (s (s z))) R.
%   % => No solution to %solve found

double : nat -> nat -> type.
double/z : double z z.
double/s : double (s A) (s (s R))
        <- double A R.

%solve _ : double two R.
% => _ : double two (s (s (s (s z))))
%      = double/s (double/s double/z).

double-minus-one : nat -> nat -> type.
double-minus-one/s : double-minus-one (s X) (s R)
                  <- double X R.

%solve _ : double-minus-one two R.
% => _ : double-minus-one two (s (s (s z)))
%      = double-minus-one/s (double/s double/z).

double-is-even : nat -> nat -> type.
double-is-even/z : double-is-even z z.
double-is-even/a : double-is-even A E
                <- is-nat A N
                <- double N D
                <- is-even D E.

%solve _ : double-is-even two R.
% => _ : double-is-even two (s (s (s (s z))))
%      = double-is-even/a (is-even/ss (is-even/ss is-even/z))
%                         (double/s (double/s double/z))
%                         (is-nat/s (is-nat/s is-nat/z)).

double-minus-one-is-even : nat -> nat -> type.
double-minus-one-is-even/z : double-minus-one-is-even z z.
double-minus-one-is-even/a : double-minus-one-is-even A E
                          <- is-nat A N
                          <- double-minus-one N D
                          <- is-even D E.

% %solve _ : double-minus-one-is-even two R.
% % => No solution to %solve found