Saturday 7 February 2009

Inventing a concrete syntax

ind F : .

ind T : ;
I : T.

ind Bool : ;
true : Bool;
false : Bool.

ind N : ;
O : N;
S : NN.

ind Ord :
OO : Ord;
OS : OrdOrd;
OL : (NOrd) → Ord.

ind Fin : N;
fz : (n:N)Fin (S n);
fs : (n:N)Fin nFin (S n).

ind Eq (A:)(x:A):A;
refl : Eq A x x.

ind JMEq (A:)(x:A):(B:)B;
JMrefl : JMEq A x A x.

ind So : Bool;
oh : So true.

ind Ex (T:)(P:T):;
witness : (t : T)Prf(P t) → Ex T P.

ind Acc (A:)(R:AA):A;
below : ((y:A)R y xAcc A R y) → Acc A R x.

ind W (A:)(B:A):;
sup : (a:A)(f:B aW A B)W A B.

No comments: