The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a good explanation somewhere of the level requirements for notations to factor properly?  For example, what level do I have can I substitute in for "L" in the following to make the code type-check?

Delimit Scope foo_scope with foo.

Notation "x , y" := (prod x y) (at level L, no associativity) : foo_scope.

Check (_, _). (* should be pair *)

Local Open Scope foo_scope.

Check _, _. (* should be prod *)

I've tried L = 200, and then the second check fails.  I've tried L = 199, and then the first check fails.  Is there any way to make this work?

-Jason