def
Lean.Elab.WF.getNumCandidateArgs
(fixedPrefixSize : Nat)
(preDefs : Array Lean.Elab.PreDefinition)
:
Instances For
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?
Instances For
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 α)
:
Instances For
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)
:
Instances For
def
Lean.Elab.WF.elabWFRel.generateElements
(preDefs : Array Lean.Elab.PreDefinition)
(numArgs : Array Nat)
(argCombination : Array Nat)
:
Instances For
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)
: