Documentation

Lean.Compiler.IR.Sorry

source
structure Lean.IR.Sorry.State :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lean.IR.Sorry.M (α : Type) :
    Type
    Equations
      Instances For
        source
        def Lean.IR.Sorry.visitExpr :
        Expr → ExceptT Name M Unit
        Equations
          Instances For
            source
            def Lean.IR.Sorry.visitExpr.getSorryDepFor? (f : Name) :
            ExceptT Name M Unit
            Equations
              Instances For
                source
                partial def Lean.IR.Sorry.visitFndBody (b : FnBody) :
                ExceptT Name M Unit
                source
                def Lean.IR.Sorry.visitDecl (d : Decl) :
                M Unit
                Equations
                  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)
                    Equations
                      Instances For