## Stream: Coq users

### Topic: Printing notations with patterns

#### Li-yao (Apr 05 2024 at 11:28):

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.

#### Gaëtan Gilbert (Apr 05 2024 at 11:38):

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

#### Gaëtan Gilbert (Apr 05 2024 at 11:39):

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)`

#### Li-yao (Apr 05 2024 at 11:47):

Does coq remember that I used `let '`?

#### Gaëtan Gilbert (Apr 05 2024 at 11:47):

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)

#### Gaëtan Gilbert (Apr 05 2024 at 11:47):

Li-yao said:

Does coq remember that I used `let '`?

yes

#### Li-yao (Apr 05 2024 at 11:52):

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

#### Gaëtan Gilbert (Apr 05 2024 at 11:53):

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

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

#### Gaëtan Gilbert (Apr 05 2024 at 11:58):

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

#### Li-yao (Apr 05 2024 at 12:08):

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