# Documentation

Lean.Elab.PreDefinition.WF.Rel

def Lean.Elab.WF.getNumCandidateArgs (fixedPrefixSize : Nat) (preDefs : ) :
Equations

Given a predefinition with value fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ..., where n = fixedPrefixSize, return an array A s.t. i ∈ A∈ 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 : ) (numArgs : ) (threshold : ) :
Equations
def Lean.Elab.WF.generateCombinations?.isForbidden (forbiddenArgs : ) (fidx : Nat) (argIdx : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.WF.generateCombinations?.go (forbiddenArgs : ) (numArgs : ) (threshold : ) (fidx : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel {α : Type} (preDefs : ) (unaryPreDefName : Lean.Name) (fixedPrefixSize : Nat) (argType : Lean.Expr) (wf? : ) (k : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel.go {α : Type} (preDefs : ) (unaryPreDefName : Lean.Name) (fixedPrefixSize : Nat) (k : ) (expectedType : Lean.Expr) (elements : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel.generateElements (preDefs : ) (numArgs : ) (argCombination : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.WF.elabWFRel.guess {α : Type} (preDefs : ) (unaryPreDefName : Lean.Name) (fixedPrefixSize : Nat) (k : ) (expectedType : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.