structure Lean.IR.Sorry.State : Type

• localSorryMap : Lake.NameMap Lake.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 : Lean.IR.Expr → ExceptT Lake.Name Lean.IR.Sorry.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 : Lake.Name) : ExceptT Lake.Name Lean.IR.Sorry.M Unit

Equations

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

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

def Lean.IR.Sorry.visitDecl (d : Lean.IR.Decl) : Lean.IR.Sorry.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 Lean.IR.Decl) : Lean.IR.Sorry.M Unit

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

Equations

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