Documentation

Lean.Compiler.IR.CompilerM

@[inline, reducible]
Instances For
    @[export lean_ir_log_to_string]
    Instances For
      @[inline, reducible]
      abbrev Lean.IR.CompilerM (α : Type) :
      Instances For
        @[inline]
        Instances For
          @[inline]
          Instances For
            @[inline]
            Instances For
              @[inline, reducible]
              Instances For
                @[export lean_ir_find_env_decl]
                Instances For
                  @[export lean_ir_add_decl]
                  Instances For
                    @[export lean_decl_get_sorry_dep]
                    Instances For