Documentation

Lean.Util.Sorry

source
def Lean.Expr.isSorry :
Lean.Expr → Bool
Instances For
    source
    def Lean.Expr.isSyntheticSorry :
    Lean.Expr → Bool
    Instances For
      source
      def Lean.Expr.isNonSyntheticSorry :
      Lean.Expr → Bool
      Instances For
        source
        def Lean.Expr.hasSorry (e : Lean.Expr) :
        Bool
        Instances For
          source
          def Lean.Expr.hasSyntheticSorry (e : Lean.Expr) :
          Bool
          Instances For
            source
            def Lean.Expr.hasNonSyntheticSorry (e : Lean.Expr) :
            Bool
            Instances For
              source
              def Lean.Declaration.hasSorry (d : Lean.Declaration) :
              Bool
              Instances For
                source
                def Lean.Declaration.hasNonSyntheticSorry (d : Lean.Declaration) :
                Bool
                Instances For