What determines whether a custom entry is used for printing?

Using Coq
1

Hi all.

The following is a simplified example of a problem I’m running into with custom entries:

Axiom set : string -> nat -> unit.
Axiom incr : nat -> nat.

Declare Custom Entry test.

Notation "'custom_set' a ':=' b" :=
  (set a b)
    (in custom test at level 91,
     a constr at level 1,
     b custom test at level 0).
Notation "'+1' b" :=
  (incr b)
    (in custom test at level 0,
        b constr at level 0).
Notation "'{{' e '}}'" :=
  (e) (e custom test at level 0).

Check {{ custom_set "a" := +1 0 }}.

This prints set "a" {{+1 0}}: the custom entry is used for the incr subterm but not for the set call.

How can I change the example so that it prints the whole term using custom entries? That is, how do I make it print {{ custom_set "a" := +1 0 }} instead of set "a" {{+1 0}}?

More generally, what determines at which point Coq switches to the custom entry?

Thanks a lot!

2

I’m also often confused about this. But in this case it is related to your levels. This does work:

Require Import String.

Axiom set : string -> nat -> unit.
Axiom incr : nat -> nat.

Declare Custom Entry test.

Notation "'+1' b" :=
  (incr b)
    (in custom test at level 0,
        b constr at level 0).
Notation "'custom_set' a ':=' b" :=
  (set a b)
    (in custom test at level 0,
     a constr at level 1,
     b custom test at level 0).
Notation "'{{' e '}}'" :=
  e (e custom test at level 0).

Check {{ custom_set "a" := +1 0 }}.
3

Thanks! Indeed, tweaking levels often helps… but is there a general rule or insight behind this?

(if needed I can provide a larger example in which adding levels only seems to make some cases work, but not all)

4

Well, I’m not an expert. But I assume that the rule is that a notation is only printed when the current level is higher or equal to the level of that notation. For example, the following modification of your code also works:

Require Import String.

Axiom set : string -> nat -> unit.
Axiom incr : nat -> nat.

Declare Custom Entry test.

Notation "'custom_set' a ':=' b" :=
  (set a b)
    (in custom test at level 91,
     a constr at level 1,
     b custom test at level 0).
Notation "'+1' b" :=
  (incr b)
    (in custom test at level 0,
        b constr at level 0).
Notation "'{{' e '}}'" :=
  (e) (e custom test at level 91).

Check {{ custom_set "a" := +1 0 }}.
1 Like
5

Oh, and this bug is also something to look out for: https://github.com/coq/coq/issues/13018

6

Thanks, this is very helpful!