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 lhs rhs : 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.unfoldPredRelMutual (eqnInfo : EqnInfo) (body : Expr) (reduceConclusion : Bool := false) : MetaM (Array Expr)

Unfolds a PartialOrder relation between tuples of predicates into an array of quantified implications.

This function handles mutual recursion cases where we have a tuple of predicates being compared. For each predicate in the tuple it projects out the corresponding components from both sides of the relation and unfolds the partial order relation into quantified implications using unfoldPredRel

Parameters:

• eqnInfo: Equation information containing declaration names and fixpoint types for each predicate in the mutual block
• body: The partial order relation expression to unfold
• reduceConclusion: Optional parameter (defaults to false) that determines whether to perform weak head normalization on the conclusion

Returns: An array of expressions, where each element represents the unfolded implication for the corresponding predicate in the mutual block.

Equations

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

def Lean.Elab.PartialFixpoint.getInductionPrinciplePostfix (name : Name) (isMutual : Bool) : MetaM Name

Equations

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

def Lean.Elab.PartialFixpoint.deriveInduction (name : Name) (isMutual : Bool) : 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.