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 2012-04-26 18:48

https://sympa-roc.inria.fr/wws/arc/coq-club/2012-01/msg00146.html
Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List
All trademarks and copyrights on this site are owned by their respective parties. All comments and posts are the responsibility of their own posters.
- Tinychan + 2ch Mode -