Documentation

Lean.Elab.PreDefinition.TerminationArgument

This module contains

Elaborated form for a termination_by clause.

The fn has the same (value) arity as the recursive functions (stored in arity), and maps its arguments (including fixed prefix, in unpacked form) to the termination argument.

If structural := Bool, then the fn is a lambda picking out exactly one argument.

Instances For
    Equations
    @[reducible, inline]

    A complete set of TerminationArguments, as applicable to a single clique.

    Equations
    Instances For

      Elaborates a TerminationBy to an TerminationArgument.

      • type is the full type of the original recursive function, including fixed prefix.
      • hint : TerminationBy is the syntactic TerminationBy.
      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.TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Lean.Elab.TerminationArgument) :
          Lean.MetaM (Lean.TSyntax `Lean.Parser.Termination.terminationBy)

          Delaborates a TerminationArgument back to a TerminationHint, e.g. for termination_by?.

          This needs extra information:

          • arity is the value arity of the recursive function
          • extraParams indicates how many of the functions arguments are bound “after the colon”.
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[irreducible]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For