Documentation

ImportGraph.Util.FindSorry

source
def ImportGraph.allConstantsWithSorry (env : Lean.Environment) :
Lean.NameSet

Array of all constant names which contain a sorry.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def ImportGraph.allModulesWithSorry (env : Lean.Environment) :
    Lean.NameSet

    Array of all module names of modules containing at least one sorry.

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