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

Equations

• Lean.Expr.isSorry _fun_discr = match _fun_discr 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 _fun_discr = match _fun_discr 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 _fun_discr = match _fun_discr 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 a => Lean.Expr.isConstOf a (Lean.Name.mkStr1 "sorryAx")) e)

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

Equations

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

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

Equations

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

partial def Lean.MessageData.hasSorry : Lean.MessageData → Bool

partial def Lean.MessageData.hasSyntheticSorry (msg : Lean.MessageData) : Bool

partial def Lean.MessageData.hasSyntheticSorry.visit : Lean.MessageData → Bool

def Lean.Exception.hasSyntheticSorry : Lean.Exception → Bool

Equations

• Lean.Exception.hasSyntheticSorry _fun_discr = match _fun_discr with | Lean.Exception.error ref msg => Lean.MessageData.hasSyntheticSorry msg | x => false

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

Equations

• Lean.Declaration.hasSorry d = Id.run (Lean.Declaration.foldExprM d (fun r e => 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 e => r || Lean.Expr.hasNonSyntheticSorry e) false)