structure Lean.IR.Sorry.State : Type

• localSorryMap : NameMap Name
• modified : Bool

@[reducible, inline]

abbrev Lean.IR.Sorry.M (α : Type) : Type

Equations

• Lean.IR.Sorry.M = StateT Lean.IR.Sorry.State Lean.IR.CompilerM

def Lean.IR.Sorry.visitExpr : Expr → ExceptT Name M Unit

Equations

• Lean.IR.Sorry.visitExpr (Lean.IR.Expr.fap f ys) = Lean.IR.Sorry.visitExpr.getSorryDepFor? f
• Lean.IR.Sorry.visitExpr (Lean.IR.Expr.pap f ys) = Lean.IR.Sorry.visitExpr.getSorryDepFor? f
• Lean.IR.Sorry.visitExpr x✝ = pure ()

def Lean.IR.Sorry.visitExpr.getSorryDepFor? (f : Name) : ExceptT Name M Unit

Equations

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

partial def Lean.IR.Sorry.visitFndBody (b : FnBody) : ExceptT Name M Unit

def Lean.IR.Sorry.visitDecl (d : Decl) : M Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.Sorry.visitDecl d = pure ()

partial def Lean.IR.Sorry.collect (decls : Array Decl) : M Unit

def Lean.IR.updateSorryDep (decls : Array Decl) : CompilerM (Array Decl)

Equations

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