The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

Dans son message du Monday 15 February, Randy Pollack a écrit : 
> 
>   Coq < Fixpoint test [a:Prop][b:Set] : Set := b.
>   Toplevel input, characters 23-24
>   > Fixpoint test  [a:Prop][b:Set] : Set := b.
>   >                        ^
>   Syntax error: ':' expected after ']' (in [Vernac.onerec])
> 
>   Coq < Fixpoint test [a:Prop;b:Set] : Set := b.
>   Warning: test is non-recursively defined
> 
> You probably don't consider this a bug, but if "[a:Prop][b:Set]" and
> "[a:Prop;b:Set]" mean the same thing, why can't they both be parsed?
> 
> Randy

It is not the same thing, indeed. "[a:Prop][b:Set]t" and
"[a:Prop;b:Set]t", where t is a term, are two different notations for
the same term.

But in the commands "Fixpoint test [a:foo;b:bar] := t" and 
"Fixpoint test [a:foo] := [b:bar]t" are different. In the first one,
the recursive arguement is "b" and it is "a" in the second one.

If we accept the syntax "Fixpoint test  [a:Prop][b:Set]" as a
shorthand for "Fixpoint test [a:Prop; b:Set]" the difference between
"Fixpoint test  [a:Prop][b:Set] := t" and "Fixpoint test [a:foo] := [b:bar]t"
will be hard to explain.

Another point I didn't mention in my previous mail : thank you for
your comments and remarks. Feedback is always welcome.

Patrick Loiseleur

-- 
Patrick.Loiseleur AT lri.fr