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

**URL:** <https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071>\
**Category:** Using Rocq\
**Tags:** notation\
**Created:** [October 5, 2020, 5:00pm UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071 "2020-10-05T17:00:01Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [October 5, 2020, 5:00pm UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071/1 "2020-10-05T17:00:01Z")

</div>

Hi all.

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

```coq
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!

---

<div class="post-metadata">

**Author:** ![Lasse](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lasse/32/413_2.png) [@Lasse](https://discourse.rocq-prover.org/u/Lasse)\
**Post date:** [October 5, 2020, 6:04pm UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071/2 "2020-10-05T18:04:30Z")

</div>

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

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

```

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [October 5, 2020, 6:53pm UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071/3 "2020-10-05T18:53:59Z")

</div>

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)

---

<div class="post-metadata">

**Author:** ![Lasse](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lasse/32/413_2.png) [@Lasse](https://discourse.rocq-prover.org/u/Lasse)\
**Post date:** [October 5, 2020, 7:11pm UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071/4 "2020-10-05T19:11:57Z")

</div>

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:

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

```

---

<div class="post-metadata">

**Author:** ![Lasse](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lasse/32/413_2.png) [@Lasse](https://discourse.rocq-prover.org/u/Lasse)\
**Post date:** [October 6, 2020, 3:07am UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071/5 "2020-10-06T03:07:21Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [October 6, 2020, 4:09am UTC](https://discourse.rocq-prover.org/t/what-determines-whether-a-custom-entry-is-used-for-printing/1071/6 "2020-10-06T04:09:44Z")

</div>

Thanks, this is very helpful!