Documentation

Lean.Compiler.IR.Sorry

source
structure Lean.IR.Sorry.State :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.IR.Sorry.M (α : Type) :
    Type
    Instances For
      source
      def Lean.IR.Sorry.visitExpr :
      Expr → ExceptT Name M Unit
      Instances For
        source
        partial def Lean.IR.Sorry.visitFnBody (b : FnBody) :
        ExceptT Name M Unit
        source
        def Lean.IR.Sorry.visitDecl (d : Decl) :
        M Unit
        Instances For
          source
          partial def Lean.IR.Sorry.collect (decls : Array Decl) :
          M Unit
          source
          def Lean.IR.updateSorryDep (decls : Array Decl) :
          CompilerM (Array Decl)
          Instances For