def Lean.Elab.PartialFixpoint.mkAdmAnd (α instα adm₁ adm₂ : Expr) : MetaM Expr

partial def Lean.Elab.PartialFixpoint.mkAdmProj (packedInst : Expr) (i : Nat) (e : Expr) : MetaM Expr

def Lean.Elab.PartialFixpoint.CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr

def Lean.Elab.PartialFixpoint.unfoldPredRel (predType body : Expr) (fixpointType : PartialFixpointType) (reduceConclusion : Bool := false) : MetaM Expr

Unfolds an appropriate PartialOrder instance on predicates to quantifications and implications. I.e. ImplicationOrder.instPartialOrder.rel P Q becomes ∀ x y, P x y → Q x y.

In the premise of the Park induction principle (lfp_le_of_le_monotone) we use a monotone map defining the predicate in the eta expanded form. In such a case, besides desugaring the predicate, we need to perform a weak head reduction. The optional parameter reduceConclusion (false by default) indicates whether we need to perform this reduction.

def Lean.Elab.PartialFixpoint.deriveInduction (name : Name) : MetaM Unit

def Lean.Elab.PartialFixpoint.isInductName (env : Environment) (name : Name) : Bool

def Lean.Elab.PartialFixpoint.isOptionFixpoint (env : Environment) (name : Name) : Bool

Returns true if name defined by partial_fixpoint, the first in its mutual group, and all functions are defined using the CCPO instance for Option.

def Lean.Elab.PartialFixpoint.isPartialCorrectnessName (env : Environment) (name : Name) : Bool

def Lean.Elab.PartialFixpoint.mkOptionAdm (motive : Expr) : MetaM Expr

Given motive : α → β → γ → Prop, construct a proof of admissible (fun f => ∀ x y r, f x y = r → motive x y r)

def Lean.Elab.PartialFixpoint.derivePartialCorrectness (name : Name) : MetaM Unit