coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nuno Gaspar <nmpgaspar AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] bug or feature
- Date: Fri, 2 Aug 2013 18:03:29 +0200
Hello.
I believe this is a bug, but then again probably it would have been noticed by now..Inductive one : Prop := True.
Inductive two : Prop := True.
Error: True already exists.Sure, you could say that I shouldn't use Inductive in such cases, but still... (I noticed while using this 'Inductive' as a placeholder)
--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.
- [Coq-Club] bug or feature, Nuno Gaspar, 08/02/2013
- Re: [Coq-Club] bug or feature, Adam Chlipala, 08/02/2013
- Re: [Coq-Club] bug or feature, Nuno Gaspar, 08/02/2013
- Re: [Coq-Club] bug or feature, Kristopher Micinski, 08/02/2013
- Re: [Coq-Club] bug or feature, Nuno Gaspar, 08/02/2013
- Re: [Coq-Club] bug or feature, Adam Chlipala, 08/02/2013
Archive powered by MHonArc 2.6.18.