Hi, I am very confused by how the printing of patterns in binders works. Can someone explain why the same term is printed in two different ways in the following example?

```
Axiom get_tuple : forall (T : (nat * nat * nat) -> Prop), Prop.
Goal get_tuple (fun '(x1, x2, x3) => x1 = 0).
Proof.
Set Printing All.
(* Copy term from goal: *)
pose (get_tuple
(fun pat : prod (prod nat nat) nat =>
match pat return Prop with
| pair p _ => match p return Prop with
| pair x1 _ => @eq nat x1 O
end
end)).
(* The body of P and the goal print identical now. *)
Unset Printing All.
(* But now they print differently. What is going on? *)
Abort.
```

matches remember how they were generated (`'(pattern)`

, `(_, _)`

tuple, `if`

or plain `match`

) and use the same way to print

Additionally "plain `match`

" can be overriden by some options depending on the type,

for instance `prod`

is in the https://coq.github.io/doc/master/refman/language/extensions/match.html#printing-matching-on-irrefutable-patterns table so by default matches on prod get printed as `let (_, ..., _) := ...`

I see, thanks for the explanation. Is there a way to copy this information from one constr to another using Ltac or Ltac2?

in ltac2 there's the Constr.Unsafe.case type which contains that info

do take care that a value of that type is specific to the inductive that is matched on

I think that works for my use case, thanks!

Last updated: Jun 13 2024 at 19:02 UTC