The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

You have it backwards: the constructor is I, True is the thing in the Prop:

Inductive True : Prop :=  I : True

Kris

On Fri, Aug 2, 2013 at 12:13 PM, Nuno Gaspar 
<nmpgaspar AT gmail.com>
 wrote:
> ohh, I get it now, lol
>
> My confusion was due to the fact that I meant True as the one in Prop, and
> not a constructor element :x
>
>
> 2013/8/2 Adam Chlipala 
> <adamc AT csail.mit.edu>
>>
>> It doesn't look like a bug to me.  Coq uniformly enforces a rule that a
>> given "global" identifier may only be defined once per scope (e.g., module)
>> that permits "global" identifier definitions.
>>
>>
>> On 08/02/2013 12:03 PM, Nuno Gaspar wrote:
>>>
>>> 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.
>>>
>>> You won't be able to evaluate the second definition.
>
>
>
>
> --
> 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.