Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

Hot stripping coqs

Name: Anonymous 2012-04-26 17:03

Hello proggers.

How do I discharge this goal in Coq?

Inductive type : nat -> Set := ctor : forall n, type n.
Goal forall n, type 0 <> type (S n).

Name: Anonymous 2013-06-18 8:08

Goddamnit, why did you have to bump this thread? Any minute now L.A.Calculus is going to show up and call us all MATH NERDS and STACK BOYZ.

Newer Posts