There is a minor typo in https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Extending-Lean___s-Output/#delaborators. It talks about a "SubExp" namespace, where only "SubExpr" seems to exist (and have the mentioned functions).
There is a minor typo in https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Extending-Lean___s-Output/#delaborators. It talks about a "SubExp" namespace, where only "SubExpr" seems to exist (and have the mentioned functions).