pp.beta

Stream: lean4

[Sebastian Reichelt]

Does Lean 4 have something equivalent to set_option pp.beta true in Lean 3? It would be very useful for me. Some other pp options work, but I haven't been able to find a list.

[Bryan Gin-ge Chen]

You can generate a list of the options using this snippet (maybe something built-in has been added to Lean 4 since then, not sure).

[Sebastian Reichelt]

Thank you! Interestingly, pp.beta does appear in your list, but when I try it, I get "unknown option pp.beta" (with current nightly).

[Bryan Gin-ge Chen]

It seems that it was removed since Lean 4.0.0-m1. Here's the output from the latest nightly.

[Alexander Bentkamp]

(deleted)

[Leonardo de Moura]

Added an issue for it: https://github.com/leanprover/lean4/issues/715
It will be implemented soon.

[Alexander Bentkamp]

I'd like to share my solution for this until it's supported officially:

import Lean

open Lean PrettyPrinter Delaborator SubExpr

@[delab app]
def delabFoo : Delab := do
  let e ← getExpr
  if e.isHeadBetaTarget
  then
    return ← delab e.headBeta
  else
    failure