def Lean.Elab.WF.getNumCandidateArgs (fixedPrefixSize : Nat) (preDefs : Array Lean.Elab.PreDefinition) : Lean.MetaM (Array Nat)

Equations

• Lean.Elab.WF.getNumCandidateArgs fixedPrefixSize preDefs = Array.mapM (fun preDef => Lean.Meta.lambdaTelescope preDef.value fun xs x => pure (Array.size xs - fixedPrefixSize)) preDefs

def Lean.Elab.WF.getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : Lean.Elab.PreDefinition) : Lean.MetaM (Array Nat)

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) : Option (Array (Array Nat))

Equations

• Lean.Elab.WF.generateCombinations? forbiddenArgs numArgs threshold = some (StateT.run (Lean.Elab.WF.generateCombinations?.go forbiddenArgs numArgs threshold 0 #[]) #[]).snd

def Lean.Elab.WF.generateCombinations?.isForbidden (forbiddenArgs : Array (Array Nat)) (fidx : Nat) (argIdx : Nat) : Bool

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) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit

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 : Lake.Name) (fixedPrefixSize : Nat) (argType : Lean.Expr) (wf? : Option Lean.Elab.WF.TerminationWF) (k : Lean.Expr → Lean.Elab.TermElabM α) : Lean.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 : Lake.Name) (fixedPrefixSize : Nat) (k : Lean.Expr → Lean.Elab.TermElabM α) (expectedType : Lean.Expr) (elements : Array Lean.Elab.WF.TerminationByElement) : Lean.Elab.TermElabM α

Equations

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

def Lean.Elab.WF.elabWFRel.generateElements (preDefs : Array Lean.Elab.PreDefinition) (numArgs : Array Nat) (argCombination : Array Nat) : Lean.Elab.TermElabM (Array Lean.Elab.WF.TerminationByElement)

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 : Lake.Name) (fixedPrefixSize : Nat) (k : Lean.Expr → Lean.Elab.TermElabM α) (expectedType : Lean.Expr) : Lean.Elab.TermElabM α

Equations

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