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

Returns true if the expression is an application of sorryAx.

Equations

• e.isSorry = e.isAppOf `sorryAx

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

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

Equations

• e.isSyntheticSorry = (e.isAppOf `sorryAx && decide (e.getAppNumArgs ≥ 2) && (e.getArg! 1).isConstOf `Bool.true)

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

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

Equations

• e.isNonSyntheticSorry = (e.isAppOf `sorryAx && decide (e.getAppNumArgs ≥ 2) && (e.getArg! 1).isConstOf `Bool.false)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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