[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

TCCs



Hi,
	When I type check the following theory, 
ud_list_theory [T : TYPE+ ] : THEORY

BEGIN
	ud_list : TYPE+
        l: VAR ud_list 
        e, x : VAR T

	null : ud_list
	cons?(l) : bool = l /= null
	
	cons : [T, ud_list -> (cons?)]
	car  : [(cons?) -> T]
	cdr  : [(cons?) -> ud_list ]
	
	car_cons : axiom car(cons(e, l)) = e
	cdr_cons : axiom cdr(cons(e, l)) = l
	
	car_cdr_cons : theorem car(cdr(cons(x,cons(e,l))))= e
END ud_list_theory

I get the following tccs eventhough I have put TYPE+.
How to discharge or prove these tccs?
I would appreciate any help.
Thanks
Magesh