display coercions more usefully

Stream: new members

[Michael George]

I'm working on some proofs that different casting operators behave nicely. I'm finding it quite hard to reason about goals like (↑↑x.hi.toNat).toNat = x.hi.toNat because I can't keep track of the overloadings of ↑. Is there a way to display this as something like (((x.hi.toNat) : \N) : \Z) = x.hi.toNat? I've tried set_option pp.coercions false, but it doesn't help a lot because it just changes this to x.hi.toNat.cast.cast.toNat`, which doesn't really help.

[Patrick Massot]

You can try using a custom delaborator. But I can’t help you more without a #mwe

[Patrick Massot]

A super ad-hoc solution applying only to Nat.cast would be to put in your code:

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Nat.cast]
def natCastDelab : Delab := do
  let α ← withNaryArg 0 delab
  let x ← withNaryArg 2 delab
  `(($x : $α))

[Patrick Massot]

And you can throw in a guard <| (← getExpr).isAppOfArity ``Nat.cast 3 somewhere in case you have unapplied Nat.cast floating around.