def
Lean.Elab.WF.getNumCandidateArgs
(fixedPrefixSize : Nat)
(preDefs : Array Lean.Elab.PreDefinition)
:
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)
:
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
- Lean.Elab.WF.generateCombinations? forbiddenArgs numArgs threshold = some (StateT.run (Lean.Elab.WF.generateCombinations?.go forbiddenArgs numArgs threshold 0 #[]) #[]).snd
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.Expr → 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 : Lean.Name)
(fixedPrefixSize : Nat)
(k : Lean.Expr → Lean.Elab.TermElabM α)
(expectedType : Lean.Expr)
(elements : Array Lean.Elab.WF.TerminationByElement)
:
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)
:
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.Expr → Lean.Elab.TermElabM α)
(expectedType : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.