Documentation

Lean.Compiler.LCNF.PrettyPrinter

@[reducible, inline]
Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              def Lean.Compiler.LCNF.PP.run {α : Type} (x : M α) :
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For

                                                              Execute x in CoreM without modifying Cores state. This is useful if we want make sure we do not affect the next free variable id.

                                                              Equations
                                                                Instances For

                                                                  Similar to ppDecl, but in CoreM, and it does not assume decl has already been internalized. This function is used for debugging purposes.

                                                                  Equations
                                                                    Instances For

                                                                      Similar to ppCode, but in CoreM, and it does not assume code has already been internalized.

                                                                      Equations
                                                                        Instances For