The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 26 May 2011 10:41:58 +0200,
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 a écrit :

> Hi all, I don't understand why the first definition is accepted and
> not the second one.
> 
> Inductive bool_comp (b: bool): bool -> Prop :=
> | Opp: forall q, (if b
>                  then match q with true => False | false => True end
>                  else match q with true => True | false => False end)
>                  -> bool_comp b q.
> 
> Print bool_comp.
> Inductive bool_comp2 (b: bool): bool -> Prop :=
> | Opp2: forall q, (match b return Prop with
>                  | true => match q return Prop with true => False |
> false => True end | false => match q return Prop with true => True |
> false => False end end) -> bool_comp2 b q.

And by the way, in the second case, I really don't understand what
could be the reason to refuse it, as the result type is outside of the
result type, since you can make a definition from the "match ... end",
and then use it inside the inductive.

(I could understand to refuse
"Inductive pred (d: nat): nat -> Prop :=
 | Pred: match d with O => pred d O | S n => pred d n end".
but it is noth the case here.)