Documentation

Lean.Elab.PreDefinition.TerminationHint

Support for termination_by notation #

A single termination_by clause

  • structural : Bool
  • vars : Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole]
  • body : Lean.Term
  • synthetic : Bool

    If synthetic := true, then this termination_by clause was generated by GuessLex, and vars refers to all parameters of the function, not just the “extra parameters”. Cf. Lean.Elab.WF.unpackUnary

Instances For
    Equations

    A single decreasing_by clause

    Instances For
      Equations

      The termination annotations for a single function. For decreasing_by, we store the whole decreasing_by tacticSeq expression, as this is what Term.runTactic expects.

      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Instances For

          Logs warnings when the TerminationHints are unexpectedly present.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            True if any form of termination hint is present.

            Equations
            • hints.isNotNone = (hints.terminationBy??.isSome || hints.terminationBy?.isSome || hints.decreasingBy?.isSome)
            Instances For

              Remembers extraParams for later use. Needs to happen early enough where we still know how many parameters came from the function header (headerParams).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Checks that termination_by binds at most as many variables are present in the outermost lambda of value, and throws appropriate errors.

                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.elabTerminationHints {m : TypeType} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Lean.Parser.Termination.suffix) :

                    Takes apart a Termination.suffix syntax object

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For