Documentation

Lean.Compiler.IR.Sorry

source
structure Lean.IR.Sorry.State :
Type
Instances For
    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.