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.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.