%
% twelf signature for INCLL
%

sort : type.
arrow : sort -> sort -> sort.
cross : sort -> sort -> sort.
trm : sort -> type. 
app : trm (arrow A B) -> trm A -> trm B.
lam : (trm A -> trm B) -> trm (arrow A B).
pair : trm A -> trm B -> trm (cross A B).

eval : trm A -> trm A -> type.
eval_lam : eval (lam E) (lam E).
eval_app : eval (app (lam E) E') V 
	<- eval E' V'
	<- eval (E V') V.

atm : type.
frm : type.

int : sort.

1 : trm int.
2 : trm int.
3 : trm int.
4 : trm int.
5 : trm int.

list : sort -> sort.

nil : trm (list A).
| : trm A -> trm (list A) -> trm (list A). %infix right 30 |.



^ : atm -> frm. %prefix 50 ^. 

=> : frm -> frm -> frm. %infix right 20 =>.
=0 : frm -> frm -> frm. %infix right 20 =0.
=>> : frm -> frm -> frm. %infix right 20 =>>.
>=> : frm -> frm -> frm. %infix right 20 >=>.
forall : {s} (trm s -> frm) -> frm. 
forall2 : {s1} {s2} ((trm s1 -> trm s2) -> frm) -> frm. 

<= = [x] [y] y => x. %infix left 10 <=.
0= = [x] [y] y =0 x. %infix left 10 0=.
<<= = [x] [y] y =>> x. %infix left 10 <<=.
<=< = [x] [y] y >=> x. %infix left 10 <=<.