search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.69k stars 421 forks source link

rfc: moving `Lean.PrettyPrinter.Delaborator.SubExpr` to `Lean.SubExpr` #1183

Closed EdAyers closed 2 years ago

EdAyers commented 2 years ago

I have found metaprogramming uses for Lean.SubExpr outside of the delaborator. However it feels strange to write new methods for SubExpr in the Lean.PrettyPrinter.Delaborator namespace. Would you accept a PR to move it to the Lean namespace?

leodemoura commented 2 years ago

Yes!

leodemoura commented 2 years ago

and thanks for asking.