From c8a2a51063dfc25ac10e2a0a0babf4c9aa720c0b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 3 Dec 2025 10:35:06 +0100 Subject: [PATCH] =?UTF-8?q?fix:=20missing=20words=20in=20=E2=80=9CElaborat?= =?UTF-8?q?ion=20Results=E2=80=9D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This fixes #681 --- Manual/Elaboration.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 367fd5e0..b4bafb8d 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -278,7 +278,7 @@ fun {α} motive x h_1 h_2 => :::paragraph The pre-definition is then sent to the compiler and to the kernel. The compiler receives the pre-definition as-is, with recursion intact. -The version sent to the kernel, on the other hand, undergoes a second transformation that replaces explicit recursion with {ref "structural-recursion"}[uses of recursors], {ref "well-founded-recursion"}[well-founded recursion], or . +The version sent to the kernel, on the other hand, undergoes a second transformation that replaces explicit recursion with {ref "structural-recursion"}[uses of recursors], {ref "well-founded-recursion"}[well-founded recursion], or {ref "partial-fixpoint"}[partial fixpoint recursion]. This split is for three reasons: * The compiler can compile {ref "partial-unsafe"}[`partial` functions] that the kernel treats as opaque constants for the purposes of reasoning. * The compiler can also compile {ref "partial-unsafe"}[`unsafe` functions] that bypass the kernel entirely.