Infoview `.1` and `.2`

Stream: mathlib4

[Martin Dvořák]

Can I stop Infoview from displaying .1 and .2 please?
I want to see .fst and .snd and another time .left and .right and so on.

[Asei Inoue]

i’m also interested in this

[Patrick Massot]

I’m not sure you can unregister a delaborator, but you can shadow it by declaring a new one later:

import Mathlib.Tactic

variable (x : ℕ × ℕ)

#check x.1

open Lean PrettyPrinter Delaborator
/-- Delaborator for `Prod.fst x` as `x.fst`. -/
@[app_delab Prod.fst]
def delabProdFst : Delab := withOverApp 3 do
  let x ← SubExpr.withAppArg delab
  `($(x).$(mkIdent `fst))

/-- Delaborator for `Prod.snd x` as `x.snd`. -/
@[app_delab Prod.snd]
def delabProdSnd : Delab := withOverApp 3 do
  let x ← SubExpr.withAppArg delab
  `($(x).$(mkIdent `snd))

#check x.1

#check x.2

[Martin Dvořák]

I guess I'll redeclare all of them then.

[Notification Bot]

This topic was moved here from #lean4 > Infoview .1 and .2 by Kyle Miller.

[Kyle Miller]

Overriding delaborators works, but it's not a great solution (it's a bit delicate) — why not make the mathlib ones be configurable with a new pp option?

As far as I know, only Prod.fst and Prod.snd have such delaborators. Where are you seeing .left and .right print as .1 and .2?

[Kyle Miller]

mathlib4#20455

[Kyle Miller]

By the way, you can disable delaborators locally for a given module.

import Mathlib.Tactic

variable (x : ℕ × ℕ)

#check x.1
-- x.1 : ℕ

attribute [-delab] Prod.delabProdFst Prod.delabProdSnd

#check x.1
-- x.fst : ℕ

#check x.2
-- x.snd : ℕ

[Eric Wieser]

It would be cool if the infoview had some way to inspect which delaborator was responsible for a certain pretty-printed syntax, assuming that's a meaningful question

[Kyle Miller]

That's (mostly) meaningful, and it could be recorded. Maybe the Infoview could have a debug option to enable viewing this information (if/when it exists)?

[Martin Dvořák]

[edit: I already have pp.numericProj.prod available. Thank a lot!]