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

Equations

• Lean.Elab.PartialFixpoint.mkAdmAnd α instα adm₁ adm₂ = Lean.Meta.mkAppOptM `Lean.Order.admissible_and #[some α, some instα, none, none, some adm₁, some adm₂]

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.PartialFixpoint.isInductName env (pre.str n) = (pure false).run
• Lean.Elab.PartialFixpoint.isInductName env name = (pure false).run

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.PartialFixpoint.isPartialCorrectnessName env name = (pure false).run

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.