Documentation

Lean.Elab.PreDefinition.WF.Rel

Equations

Given a predefinition with value fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ..., where n = fixedPrefixSize, return an array A s.t. i ∈ A iff sizeOf yᵢ reduces to a literal. This is the case for types such as Prop, Type u, etc. This arguments should not be considered when guessing a well-founded relation. See generateCombinations?

Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : optParam Nat 32) :
Equations
def Lean.Elab.WF.generateCombinations?.isForbidden (forbiddenArgs : Array (Array Nat)) (fidx : Nat) (argIdx : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.generateCombinations?.go (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : optParam Nat 32) (fidx : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel {α : Type} (preDefs : Array Lean.Elab.PreDefinition) (unaryPreDefName : Lean.Name) (fixedPrefixSize : Nat) (argType : Lean.Expr) (wf? : Option Lean.Elab.WF.TerminationWF) (k : Lean.ExprLean.Elab.TermElabM α) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel.go {α : Type} (preDefs : Array Lean.Elab.PreDefinition) (unaryPreDefName : Lean.Name) (fixedPrefixSize : Nat) (k : Lean.ExprLean.Elab.TermElabM α) (expectedType : Lean.Expr) (elements : Array Lean.Elab.WF.TerminationByElement) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel.guess {α : Type} (preDefs : Array Lean.Elab.PreDefinition) (unaryPreDefName : Lean.Name) (fixedPrefixSize : Nat) (k : Lean.ExprLean.Elab.TermElabM α) (expectedType : Lean.Expr) :
Equations
  • One or more equations did not get rendered due to their size.