I have two definitions that appear *identical* with `Set Printing All`

(even the variable names!). Yet they show up differently with notations enabled. Is there some internal state that the pretty-printer uses to decide what notation to use, that can't be seen with `Set Printing All`

?

For more details, I have a notation for a monadic `bind`

```
Notation "'let+' x := u 'in' v" := (bind u (fun x => v))
(at level 200, x pattern) : otick_scope.
```

which lets me bind patterns `let+ (x,y) := foo in bar x y`

, which under the hood is desugared to `bind u (fun pat => match pat with (x, y) => bar x y end)`

.

For one definition it prints `let+ (d0, d1) := unConsA d in OTick.ret (d0, d1)`

. For the other definition it prints `let+ pat := unConsA d in (let (d0, d1) := pat in OTick.ret (d0, d1))`

. AFAICT both desugar to the same term, so they should be printed the same.

can reproduce with

```
Axiom M : Type -> Type.
Axiom bind : forall {A B}, M A -> (A -> M B) -> M B.
Axiom ret : forall {A}, A -> M A.
Notation "'let+' x := u 'in' v" :=
(bind u (fun x => v))
(at level 200, x pattern).
Check fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1).
(* fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1) *)
(* fun d : M (prod nat nat) =>
@bind (prod nat nat) (prod nat nat) d
(fun pat : prod nat nat =>
match pat return (M (prod nat nat)) with
| pair d0 d1 => @ret (prod nat nat) (@pair nat nat d0 d1)
end)
*)
Check fun d : M (nat * nat) => let+ pat := d in (let (d0, d1) := pat in ret (d0, d1)).
(* fun d : M (nat * nat) => let+ pat := d in (let (d0, d1) := pat in ret (d0, d1)) *)
(* fun d : M (prod nat nat) =>
@bind (prod nat nat) (prod nat nat) d
(fun pat : prod nat nat =>
match pat return (M (prod nat nat)) with
| pair d0 d1 => @ret (prod nat nat) (@pair nat nat d0 d1)
end)
*)
```

first comment is default printing, second is Set Printing All

it's probably the case style as

```
Check fun d : M (nat * nat) => let+ pat := d in (let '(d0, d1) := pat in ret (d0, d1)).
```

(note the `'`

in the let)

prints `fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1)`

Does coq remember that I used `let '`

?

and https://github.com/coq/coq/blob/ac1414522d0cfbdbbbd99915f0ba4eea8d3898da/theories/Init/Datatypes.v#L226 makes a match on `prod`

print as `let (_,_) :=`

by default (ie when you write a regular match)

Li-yao said:

Does coq remember that I used

`let '`

?

yes

Can I write my term without using notations so it gets printed like the first?

`Unset Printing Notations. Print (the first one).`

->

```
bind d (fun '(pair d0 d1) => ret (pair d0 d1))
```

LetPatternStyle is the only one that factorizes with lambda https://github.com/coq/coq/blob/ac1414522d0cfbdbbbd99915f0ba4eea8d3898da/interp/constrextern.ml#L1168-L1176

and I don't think there's an option to use LetPatternStyle by default so it has to be explicitly used

Because that was too easy, another challenge is to get that printing when my term is generated in elpi:

```
(* include your snippet above here *)
From elpi Require Import elpi.
Elpi Program foo lp:{{ }}.
Elpi Query lp:{{
M = {{ fun d : M (prod nat nat) => bind d (fun '(pair d0 d1) => ret (pair d0 d1)) }},
coq.elaborate-skeleton M _ M' _,
coq.env.add-const {coq.env.fresh-global-id "f"} M' _ _ _.
}}.
Print f.
(* fun d : M (nat * nat) => let+ pat := d in (let (d0, d1) := pat in ret (d0, d1)) *)
(* but I want this notation: *)
Check fun d : M (prod nat nat) => bind d (fun '(pair d0 d1) => ret (pair d0 d1)).
(* fun d : M (nat * nat) => let+ (d0, d1) := d in ret (d0, d1) *)
```

Last updated: Jun 18 2024 at 22:01 UTC