From 6998acad66900c1602baa9bf2b49ec5f3afd2577 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 2 Jan 2024 18:16:24 +0100 Subject: [PATCH] =?UTF-8?q?doc:=20fix=20typo=20=E2=80=9Creursive=E2=80=9D?= =?UTF-8?q?=20(#3131)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 447e3e5930..c9d9e9f4c2 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -224,7 +224,7 @@ def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) : /-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition, and runs the given action in the context of that call. -/ structure RecCallWithContext where - /-- Syntax location of reursive call -/ + /-- Syntax location of recursive call -/ ref : Syntax /-- Function index of caller -/ caller : Nat