def Lean.Elab.WF.checkCodomains (names : Array Name) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr) (arities : Array Nat) (termMeasures : TerminationMeasures) :
The termination measures must not depend on the varying parameters of the function, and in a mutual clique, they must be the same for all functions.
This ensures the preconditions for ArgsPacker.uncurryND.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def Lean.Elab.WF.elabWFRel {α : Type} (declNames : Array Name) (unaryPreDefName : Name) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr) (argsPacker : Meta.ArgsPacker) (argType : Expr) (termMeasures : TerminationMeasures) (k : Expr → TermElabM α) :
If the termMeasures map the packed argument argType to β, then this function passes to the
continuation a value of type WellFoundedRelation argType that is derived from the instance
for WellFoundedRelation β using invImage.
Equations
- One or more equations did not get rendered due to their size.