Skip to content

Commit 824b2b9

Browse files
authored
fix: missing words in “Elaboration Results” (#682)
This fixes #681
1 parent 1eccdcb commit 824b2b9

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Manual/Elaboration.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,7 @@ fun {α} motive x h_1 h_2 =>
278278
:::paragraph
279279
The pre-definition is then sent to the compiler and to the kernel.
280280
The compiler receives the pre-definition as-is, with recursion intact.
281-
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 .
281+
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].
282282
This split is for three reasons:
283283
* The compiler can compile {ref "partial-unsafe"}[`partial` functions] that the kernel treats as opaque constants for the purposes of reasoning.
284284
* The compiler can also compile {ref "partial-unsafe"}[`unsafe` functions] that bypass the kernel entirely.

0 commit comments

Comments
 (0)