Documentation

Mathlib.Util.PrintSorries

Tracking uses of sorry #

This file provides a #print sorries command to help find out why a given declaration is not sorry-free. #print sorries foo returns a non-sorry-free declaration bar which foo depends on, if such a bar exists.

The #print sorries in CMD combinator prints all sorries appearing in the declarations defined by the given command.

TODO #

Type of intermediate computation of sorry-tracking.

  • visited : Lean.NameSet

    The set of already visited declarations.

  • The set of sorry expressions that have been found. Note that unlabeled sorries will only be reported in the first declaration that uses them, even if a later definition independently has a direct use of sorryAx.

  • The uses of sorry that were found.

Instances For

    Collects all uses of sorry by the declaration c. It finds all transitive uses as well.

    This is a version of Lean.CollectAxioms.collect that keeps track of enough information to print each use of sorry.

    Prints all uses of sorry inside a list of declarations. Displayed sorries are hoverable and support "go to definition".

    Equations
    Instances For
      • #print sorries prints all sorries that the current module depends on.
      • #print sorries id1 id2 ... idn prints all sorries that the provided declarations depend on.
      • #print sorries in CMD prints all the sorries in declarations added by the command.

      Displayed sorries are hoverable and support "go to definition".

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

        Collects sorries in the given constants and logs a message.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          • #print sorries prints all sorries that the current module depends on.
          • #print sorries id1 id2 ... idn prints all sorries that the provided declarations depend on.
          • #print sorries in CMD prints all the sorries in declarations added by the command.

          Displayed sorries are hoverable and support "go to definition".

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