Documentation

Lean.Util.Sorry

def Lean.Expr.isSorry:

Lean.Expr → Bool

Equations

One or more equations did not get rendered due to their size.

def Lean.Expr.isSyntheticSorry:

Lean.Expr → Bool

Equations

One or more equations did not get rendered due to their size.

def Lean.Expr.isNonSyntheticSorry:

Lean.Expr → Bool

Equations

One or more equations did not get rendered due to their size.

def Lean.Expr.hasSorry:

Lean.Expr → Bool

def Lean.Expr.hasSyntheticSorry:

Lean.Expr → Bool

def Lean.Expr.hasNonSyntheticSorry:

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 _fun_discr = match _fun_discr with | Lean.Exception.error ref msg => Lean.MessageData.hasSyntheticSorry msg | x => false

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

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) :

Equations

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