This module contains the data type TerminationArgument
, the elaborated form of a TerminationBy
clause, the TerminationArguments
type for a clique and the elaboration functions.
Equations
- Lean.Elab.WF.instInhabitedTerminationArgument = { default := { ref := default, arity := default, extraParams := default, fn := default } }
@[reducible, inline]
A complete set of TerminationArgument
s, as applicable to a single clique.
Instances For
def
Lean.Elab.WF.TerminationArgument.elab
(funName : Lake.Name)
(type : Lean.Expr)
(arity : Nat)
(extraParams : Nat)
(hint : Lean.Elab.WF.TerminationBy)
:
Elaborates a TerminationBy
to an TerminationArgument
.
type
is the full type of the original recursive function, including fixed prefix.arity
is the value arity of the recursive function; the termination argument cannot take more.extraParams
is the the number of parameters the function has after the colon; together witharity
indicates how many parameters of the function are before the colon and thus in scope.hint : TerminationBy
is the syntacticTerminationBy
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.WF.TerminationArgument.delab
(termArg : Lean.Elab.WF.TerminationArgument)
:
Lean.MetaM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def
Lean.Elab.WF.TerminationArgument.delab.go :
Nat →
Lean.TSyntaxArray `ident → Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)
Equations
- One or more equations did not get rendered due to their size.