The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

You actually made nothing wrong. This is a bug, with a short fix at [1]
if ever you'd like to recompile Coq with it.

I don't see an immediate workaround, except binding also "a" in the
recursive notation, or expanding the recursive notation into a
collection of finite instances of it.

Best,

Hugo Herbelin

[1] https://github.com/coq/coq/commit/90e5945e1666540bc18e7a9b831d136041f4e487

On Mon, Sep 12, 2016 at 05:13:55PM +0300, Ilmārs Cīrulis wrote:
> Hello,
> 
> I made a notation and tested it. It was parsed correctly, but it wasn't
> display.
> Where is my mistake?
> 
> 
>     Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) 
> ..
>     (a = v))): set_scope.
>     Open Scope set_scope.
>     Check ({1, 2}).
> 
> 
> The "check" command displays
> 
>     fun a : nat => a = 1 \/ a = 2
>          : nat -> Prop
> 
> while I would like to see something like this:
> 
>     {1, 2}:  nat -> Prop
> 
> 
> 
> Thank you!
> 
> 
>