Documentation

Lean.Compiler.IR.CompilerM

Equations
Instances For
    @[reducible, inline]
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[export lean_ir_log_to_string]
        Equations
        • log.toString = log.format.pretty
        Instances For
          @[reducible, inline]
          abbrev Lean.IR.CompilerM (α : Type) :
          Equations
          Instances For
            Equations
            Instances For
              @[inline]
              Equations
              Instances For
                @[reducible, inline]
                Equations
                Instances For
                  @[export lean_ir_find_env_decl]
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          @[export lean_ir_add_decl]
                          Equations
                          Instances For
                            Equations
                            Instances For
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[export lean_decl_get_sorry_dep]
                                      Equations
                                      Instances For