From 2371222b73fe7d24e72b5244f4422818d3226409 Mon Sep 17 00:00:00 2001 From: ia0 Date: Wed, 15 Jul 2026 14:56:23 +0200 Subject: [PATCH] doc: fix bad copy/paste in PartialFixpoint --- Manual/RecursiveDefs/PartialFixpoint.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index bfa464837..324acff37 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -363,7 +363,7 @@ tag := "mutual-partial-fixpoint" Lean supports the definition of {tech}[mutually recursive] functions using {tech}[partial fixpoint]. Mutual recursion may be introduced using a {tech}[mutual block], but it also results from {keywordOf Lean.Parser.Term.letrec}`let rec` expressions and {keywordOf Lean.Parser.Command.declaration}`where` blocks. -The rules for mutual well-founded recursion are applied to a group of actually mutually recursive, lifted definitions, that results from the {ref "mutual-syntax"}[elaboration steps] for mutual groups. +The rules for mutual recursion with partial fixpoints are applied to a group of actually mutually recursive, lifted definitions, that results from the {ref "mutual-syntax"}[elaboration steps] for mutual groups. If all functions in the mutual group have the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` clause, then this strategy is used.