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

Equations

• (((Lean.Expr.const `sorryAx us).app arg).app arg_1).isSorry = true
• x.isSorry = false

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

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

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

Equations

• e.hasSorry = (Lean.Expr.find? (fun (x : Lean.Expr) => x.isConstOf `sorryAx) e).isSome

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

Equations

• e.hasNonSyntheticSorry = (Lean.Expr.find? (fun (x : Lean.Expr) => x.isNonSyntheticSorry) e).isSome

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

Equations

• d.hasSorry = (d.foldExprM (fun (r : Bool) (e : Lean.Expr) => r || e.hasSorry) false).run

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

Equations

• d.hasNonSyntheticSorry = (d.foldExprM (fun (r : Bool) (e : Lean.Expr) => r || e.hasNonSyntheticSorry) false).run