Documentation

Lean.Compiler.IR.Sorry

source
structure Lean.IR.Sorry.State:
Type
source
@[inline]
abbrev Lean.IR.Sorry.M (α : Type) :
Type
Equations
source
def Lean.IR.Sorry.visitExpr:
Lean.IR.Expr → ExceptT Lean.Name Lean.IR.Sorry.M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.IR.Sorry.visitExpr.getSorryDepFor? (f : Lean.Name) :
ExceptT Lean.Name Lean.IR.Sorry.M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.IR.Sorry.visitFndBody (b : Lean.IR.FnBody) :
ExceptT Lean.Name Lean.IR.Sorry.M Unit
source
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.
source
partial def Lean.IR.Sorry.collect (decls : Array Lean.IR.Decl) :
Lean.IR.Sorry.M Unit
source
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.