From a606c43c740f8db61307b51fe064248162adb962 Mon Sep 17 00:00:00 2001 From: MukundaKatta Date: Mon, 20 Apr 2026 00:37:03 -0700 Subject: [PATCH] docs(delab): fix 'SubExp' -> 'SubExpr' namespace typo Closes #828 --- Manual/NotationsMacros/Delab.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/NotationsMacros/Delab.lean b/Manual/NotationsMacros/Delab.lean index 97780996c..5805294a8 100644 --- a/Manual/NotationsMacros/Delab.lean +++ b/Manual/NotationsMacros/Delab.lean @@ -282,7 +282,7 @@ open Lean.PrettyPrinter.Delaborator.SubExpr :::paragraph The monad {name}`DelabM` is a {tech}[reader monad] that includes access to the current position in the {lean}`Expr`. Recursive delaboration is performed by adjusting the reader monad's tracked position, rather than by explicitly passing a subexpression to another function. -The most important functions for working with subexpressions in delaborators are in the namespace `Lean.PrettyPrinter.Delaborator.SubExp`: +The most important functions for working with subexpressions in delaborators are in the namespace `Lean.PrettyPrinter.Delaborator.SubExpr`: * {name}`getExpr` retrieves the current expression for analysis. * {name}`withAppFn` adjusts the current position to be that of the function in an application. * {name}`withAppArg` adjusts the current position to be that of the argument in an application