From 96cd6909ea5c94e8c1dd28f34a3253320abc2728 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Tue, 24 Feb 2026 15:23:58 +0100 Subject: [PATCH] doc: fix comment referring to elabElem instead of elabDoElem (#12674) --- src/Lean/Elab/Do/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean index def109a5ce..ae373d1cd7 100644 --- a/src/Lean/Elab/Do/Basic.lean +++ b/src/Lean/Elab/Do/Basic.lean @@ -105,7 +105,7 @@ inductive DoElemContKind /-- Elaboration of a `do` block `do $e; $rest`, results in a call -``elabTerm `(do $e; $rest) = elabElem e dec``, where `elabElem e ·` is the elaborator for `do` +``elabTerm `(do $e; $rest) = elabDoElem e dec``, where `elabDoElem e ·` is the elaborator for `do` element `e`, and `dec` is the `DoElemCont` describing the elaboration of the rest of the block `rest`. @@ -147,8 +147,8 @@ deriving Inhabited /-- The type of elaborators for `do` block elements. -It is ``elabTerm `(do $e; $rest) = elabElem e dec``, where `elabElem e ·` is the elaborator for `do` -element `e`, and `dec` is the `DoElemCont` describing the elaboration of the rest of the block +It is ``elabTerm `(do $e; $rest) = elabDoElem e dec``, where `elabDoElem e ·` is the elaborator for +`do` element `e`, and `dec` is the `DoElemCont` describing the elaboration of the rest of the block `rest`. -/ abbrev DoElab := TSyntax `doElem → DoElemCont → DoElabM Expr