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

Equations

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

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

Equations

• x.isSyntheticSorry = match x with | ((Lean.Expr.const `sorryAx us).app arg).app (Lean.Expr.const `Bool.true us_1) => true | x => false

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

Equations

• x.isNonSyntheticSorry = match x with | ((Lean.Expr.const `sorryAx us).app arg).app (Lean.Expr.const `Bool.false us_1) => true | x => false

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