Alpha Type.


Alpha (

      \x. \y. \x. plus x y (V x. x)
      

).

Typecheck \x. y.

Typecheck \x. \y. y.

Typecheck \x. y.

Typecheck \x. z : V y. y.

Typecheck (!(x,(a,(b:Type),c),y,[0]). Type).

Typecheck (I(x,(),y). (x, x -> x)).

Typecheck (I(x,(),_). (x, x -> x, x -> x -> x)).

Typecheck (cons 0 of (I(x,(),_). (x, x -> x, x -> x -> x))).



Typecheck ((\x. \y. x y) a b).

Typecheck ((\x. \y. \z. x y z) a b c).

Typecheck ((\x. \y. \z. x y z)).

Typecheck (x y).

Typecheck (\ (x: _). \(y: _). \(z: _). x y z).

Typecheck ((cons 1 of (I(x,(),Type).(x, x -> x))) x).

Typecheck (\x. x y).

Typecheck (\x . x).

Typecheck (\x. \y. x y).

Typecheck (!(x,(a,b,c),y,[0]). Type).

Simpl ((\x. x) (I(x,(),y). (x, x -> x))).

Simpl (
       match ((cons 1 of (I(x,(),y). (x, x -> x))) (cons 0 of (I(x,(),y). (x, x -> x)))) return (I(x,(),y). (x, x)) with
         | cons 0 of (I(x,(),y). (x, x))
         | \x. cons 1 of (I(x,(),y). (x, x))
).

Simpl (
       match (cons 0 of (I(x,(),y). (x, x -> x))) return (I(x,(),y). (x, x)) with
         | cons 0 of (I(x,(),y). (x, x))
         | \x. cons 1 of (I(x,(),y). (x, x))
).

Simpl (
       match (cons 0 of (I(x,(),y). (x, x -> x))) with
         | cons 0 of (I(x,(),y). (x, x))
         | \x. cons 1 of (I(x,(),y). (x, x))
).

Typecheck (
       match ((cons 1 of (I(x,(),y). (x, x -> x))) (cons 0 of (I(x,(),y). (x, x -> x)))) with
         | cons 0 of (I(x,(),y). (x, x))
         | \x. cons 1 of (I(x,(),y). (x, x))
).

Simpl (
       match ((cons 1 of (I(x,(),Type). (x, x -> x))) (cons 0 of (I(x,(),Type). (x, x -> x)))) with
         | cons 0 of (I(x,(),Type). (x, x))
         | \z. cons 1 of (I(x,(),Type). (x, x))
).

Simpl (
       match ((cons 1 of (I(x,(),Type). (x, x -> x))) (cons 0 of (I(x,(),Type). (x, x -> x)))) return (I(x,(),y). (x, x)) with
         | cons 0 of (I(x,(),Type). (x, x))
         | \z. cons 1 of (I(x,(),Type). (x, x))
).

Typecheck (
       match ((cons 1 of (I(x,(),Type). (x, x -> x))) (cons 0 of (I(x,(),Type). (x, x -> x)))) with
         | cons 0 of (I(x,(),Type). (x, x))
         | \z. cons 1 of (I(x,(),Type). (x, x))
).

Typecheck (
       match ((cons 1 of (I(x,(),Type). (x, x -> x))) (cons 0 of (I(x,(),Type). (x, x -> x)))) return (I(x,(),y). (x, x)) with
         | cons 0 of (I(x,(),Type). (x, x))
         | \z. cons 1 of (I(x,(),Type). (x, x))
).