HepLean 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 :
      Lean.IR.Expr → ExceptT Lake.Name Lean.IR.Sorry.M Unit
      Equations
      Instances For
        source
        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.
        Instances For
          source
          partial def Lean.IR.Sorry.visitFndBody (b : Lean.IR.FnBody) :
          ExceptT Lake.Name Lean.IR.Sorry.M Unit
          source
          def Lean.IR.Sorry.visitDecl (d : Lean.IR.Decl) :
          Lean.IR.Sorry.M Unit
          Equations
          Instances For
            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.
            Instances For