Optional delaborators

Stream: lean4

[Eric Wieser]

For debugging, it would have been helpful to me to have this delaborator:

/-- Delaborator for `no_index`. -/
@[delab mdata]
def delabNoIndex : Delab := do
  let .mdata d e ← SubExpr.getExpr | failure
  let .some (.ofBool .true) := d.find `noindex | failure
  let d := d.erase `noindex
  let inner ← withReader (fun s => {s with subExpr.expr := .mdata d e}) delab
  `(no_index $inner)

Having this enabled by default would certainly be confusing; Is the appropriate thing to do here to hide this behind a new pp option, or make the delaborator attribute scoped?

[Eric Wieser]

I found myself needed this again while debugging another consumeMData issue; could anyone advise on the scope vs pp option?

[Eric Wieser]

Or should this be enabled as a default elaborator, since it can have visible effects on (buggy) tactics?

[Eric Wieser]

Example:

import Mathlib.Tactic.Linarith

example (b : Int) (h₀ : b = -2) : b = -2           := by linarith [h₀] -- ok
example (b : Int) (h₀ : b = -2) : b = no_index(-2) := by linarith [h₀] -- failure

[Eric Wieser]

#25500 adds a refined version of the above