Documentation

Lean.Compiler.IR.CompilerM

Instances For
    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
          Instances For
            Instances For
              @[reducible, inline]
              abbrev Lean.IR.CompilerM (α : Type) :
              Equations
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    @[inline]
                    Equations
                    Instances For
                      @[inline]
                      def Lean.IR.logMessageIf {α : Type} [ToFormat α] (cls : Name) (a : α) :
                      Equations
                      Instances For
                        @[inline]
                        Equations
                        Instances For
                          @[reducible, inline]
                          Equations
                          Instances For
                            @[reducible, inline]
                            Equations
                            Instances For

                              Adds to used all Decl.fdecls referenced directly by decl.

                              Equations
                              Instances For

                                Computes the closure of Decl.fdecls referenced by decl.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Lean.IR.findEnvDecl (env : Environment) (declName : Name) :

                                  Retrieves IR for codegen purposes, i.e. independent of meta import.

                                  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]
                                                      def Lean.IR.getSorryDep (env : Environment) (declName : Name) :
                                                      Equations
                                                      Instances For