Documentation

Lean.Elab.PreDefinition.WF.TerminationArgument

This module contains the data type TerminationArgument, the elaborated form of a TerminationBy clause, the TerminationArguments type for a clique and the elaboration functions.

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.

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.
      • 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 with arity indicates how many parameters of the function are before the colon and thus in scope.
      • 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
          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