def Lean.Expr.isSorry : Lean.Expr → Bool

def Lean.Expr.isSyntheticSorry : Lean.Expr → Bool

def Lean.Expr.isNonSyntheticSorry : Lean.Expr → Bool

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

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

Equations

• e.hasSyntheticSorry = (Lean.Expr.find? (fun (x : Lean.Expr) => x.isSyntheticSorry) e).isSome

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

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

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