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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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