def Lean.Expr.isSorry (e : Expr) : Bool

Returns true if the expression is an application of sorryAx.

def Lean.Expr.isSyntheticSorry (e : Expr) : Bool

Returns true if the expression is of the form sorryAx _ true ...

def Lean.Expr.isNonSyntheticSorry (e : Expr) : Bool

Returns true if the expression is of the form sorryAx _ false ...

def Lean.Expr.hasSorry (e : Expr) : Bool

def Lean.Expr.hasSyntheticSorry (e : Expr) : Bool

def Lean.Expr.hasNonSyntheticSorry (e : Expr) : Bool

def Lean.Declaration.hasSorry (d : Declaration) : Bool

def Lean.Declaration.hasNonSyntheticSorry (d : Declaration) : Bool