Documentation

Lean.Util.Sorry

def Lean.Expr.isSorry :

Lean.Expr → Bool

Equations

Lean.Expr.isSorry x = match x with | Lean.Expr.app (Lean.Expr.app (Lean.Expr.const (Lean.Name.str Lean.Name.anonymous "sorryAx" x_6) x x_1) x_2 x_3) x_4 x_5 => 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 (Lean.Name.str Lean.Name.anonymous "sorryAx" x_7) x x_1) x_2 x_3) (Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Bool" x_8) "true" x_9) x_4 x_5) x_6 => true | x => false

def Lean.Expr.hasSorry :

Lean.Expr → Bool

def Lean.Expr.hasSyntheticSorry :

Lean.Expr → Bool

partial def Lean.MessageData.hasSorry :

Lean.MessageData → Bool

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

partial def Lean.MessageData.hasSyntheticSorry.visit :

Lean.MessageData → Bool

def Lean.Exception.hasSyntheticSorry :

Lean.Exception → Bool

Equations

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