feat: partial_fixpoint

.envrc

@@ -0,0 +1 @@
+use flake

.vale/styles/config/ignore/terms.txt

@@ -1,5 +1,6 @@
 APIs
 Abelian
+Ackermann
 Kleisli
 Packrat
 antiquotation
@@ -49,6 +50,8 @@ enum
 equational
 extensional
 extensionality
+fixpoint
+fixpoints
 functor
 functor's
 functors

Manual/Language/RecursiveDefs.lean

@@ -9,6 +9,7 @@ import VersoManual
 import Manual.Meta
 
 import Manual.Language.RecursiveDefs.Structural
+import Manual.Language.RecursiveDefs.PartialFixpoint
 
 open Verso.Genre Manual
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
@@ -29,7 +30,7 @@ Furthermore, most useful recursive functions do not threaten soundness, and infi
 Instead of banning recursive functions, Lean requires that each recursive function is defined safely.
 While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.{margin}[The section on {ref "elaboration-results"}[the elaborator's output] in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.]
 
-There are four main kinds of recursive functions that can be defined:
+There are five main kinds of recursive functions that can be defined:
 
 : Structurally recursive functions
 
@@ -47,6 +48,15 @@ There are four main kinds of recursive functions that can be defined:
   Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition.
   Even when definitional equalities exist, these functions are frequently slow to compute with because they require reducing proof terms that are often very large.
 
+: Recursive functions as fixpoints
+
+  Taking the function definition as an equation that specifies the behavior of the function, in certain cases the existence of a function satisfying this specification can be proven.
+  This strategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_.
+
+  In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness).
+
+  As with well-founded recursion, applications of functions defined via partial fixpoint are not definitionally equal to their return values.
+
 : Partial functions with nonempty ranges
 
   For many applications, it's not important to reason about the implementation of certain functions.
@@ -77,7 +87,7 @@ As described in the {ref "elaboration-results"}[overview of the elaborator's out
     If there is no such clause, then the elaborator performs a search, testing each parameter to the function as a candidate for structural recursion, and attempting to find a measure with a well-founded relation that decreases at each recursive call.
 
 This section describes the rules that govern recursive functions.
-After a description of mutual recursion, each of the four kinds of recursive definitions is specified, along with the tradeoffs between reasoning power and flexibility that go along with each.
+After a description of mutual recursion, each of the five kinds of recursive definitions is specified, along with the tradeoffs between reasoning power and flexibility that go along with each.
 
 # Mutual Recursion
 %%%
@@ -162,6 +172,8 @@ tag := "well-founded-recursion"
 This section will describe the translation of {deftech}[well-founded recursion].
 :::
 
+{include 0 Manual.Language.RecursiveDefs.PartialFixpoint}
+
 # Partial and Unsafe Recursive Definitions
 %%%
 tag := "partial-unsafe"