The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I am trying to write notations which are only for printing.  I am trying to make the following code work (in particular, I want the last line to not fail).  How do I do this?

Reserved Notation "--".

Reserved Notation "x [[ -- ]]" (at level 10).

Reserved Notation "x [[ y ]]" (at level 10, y at level 10).

Reserved Notation "A [[ x , y ]]" (at level 10, x at level 10, y at level 10).

Notation "x [[ y ]]" := ((fun _ => x) y).

Notation "--" := Set.

Notation "x [[ -- ]]" := (x).

Notation "A [[ x , y ]]" := (A (x, y)).

Check (fun xy : prod Type Type => fst xy = snd xy) [[ Set [[ -- ]] , Set ]].

Check (fun xy : prod Type Type => fst xy = snd xy) [[ Set [[ -- ]] , -- ]].

Check (fun xy : prod Type Type => fst xy = snd xy) [[ Set , -- ]].

Reserved Notation "A [[ x [[ -- ]] , y ]]" (at level 10, x at level 10, y at level 10).

Reserved Notation "A [[ x [[ -- ]] , -- ]]" (at level 10, x at level 10).

Check (fun xy : prod Type Type => fst xy = snd xy) [[ Set , -- ]].

Reserved Notation "A [[ x , -- ]]" (at level 10, x at level 10).

Check (fun xy : prod Type Type => fst xy = snd xy) [[ Set , -- ]].

 (* Unknown interpretation for notation "_ [[ _ , -- ]]". *)

As a use case for this kind of thing, suppose I want to use "--" to mean "identity" and I have a notation "a + b".  If the value "a + --" simplifies under [simpl] (but doesn't simplify fully to "a"), then I still want to display the resulting term as "a + --".  But if I make a notation for "a + --", then I have to define it to use it.  This is fine, until I want to use "+" and "--" in another scope, where defining "a + --" is unnecessary, perhaps because in this scope, the meaning of "--" is opaque.  Then I have the problem that Coq doesn't know how to interpret "a + --", even though it knew how to interpret it before the extra reserved notation.  Is there a way to fix this, for example, to declare that a notation is only for printing, or to set the levels so that things will just work with the most recently declared notation in that scope?  Or failing that, can I get notations to bind to other notations which are not yet defined (i.e., say that "(a + --)%some_scope" should parse, by default, as "(a + ( -- )%some_scope)%some_scope" for all scopes "some_scope")?

Thanks,

Jason