Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
33 lines (26 sloc) 438 Bytes
Data Nat:* = O:Nat | S:(k:Nat)Nat;
General Y;
genplus:(m:Nat)(n:Nat)Nat;
by Y;
intro PLUS m n;
induction m;
fill n;
intros;
fill S (PLUS k n);
Qed;
undefined:(A:*)A;
by Y;
intro UNDEF A;
refine UNDEF;
Qed;
Freeze undefined;
Data List (A:*) : * = nil:List A | cons:(x:A)(xs:List A)List A;
head:(A:*)(xs:List A)A;
intros;
induction xs;
refine undefined;
intros;
refine x;
Qed;
Eval head _ (cons _ O (nil Nat));
Eval head _ (nil Nat);
Something went wrong with that request. Please try again.