# What determines whether a custom entry is used for printing?

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!

``````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 }}.
``````

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)

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

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