Documentation

Lean.Compiler.LCNF.PrettyPrinter

source
@[inline, reducible]
abbrev Lean.Compiler.LCNF.PP.M (α : Type) :
Type
Instances For
    source
    def Lean.Compiler.LCNF.PP.ppFVar (fvarId : Lean.FVarId) :
    Lean.Compiler.LCNF.PP.M Lean.Format
    Instances For
      source
      def Lean.Compiler.LCNF.PP.ppExpr (e : Lean.Expr) :
      Lean.Compiler.LCNF.PP.M Lean.Format
      Instances For
        source
        def Lean.Compiler.LCNF.PP.ppArg (e : Lean.Compiler.LCNF.Arg) :
        Lean.Compiler.LCNF.PP.M Lean.Format
        Instances For
          source
          def Lean.Compiler.LCNF.PP.ppArgs (args : Array Lean.Compiler.LCNF.Arg) :
          Lean.Compiler.LCNF.PP.M Lean.Format
          Instances For
            source
            def Lean.Compiler.LCNF.PP.ppLetValue (e : Lean.Compiler.LCNF.LetValue) :
            Lean.Compiler.LCNF.PP.M Lean.Format
            Instances For
              source
              def Lean.Compiler.LCNF.PP.ppParam (param : Lean.Compiler.LCNF.Param) :
              Lean.Compiler.LCNF.PP.M Lean.Format
              Instances For
                source
                def Lean.Compiler.LCNF.PP.ppParams (params : Array Lean.Compiler.LCNF.Param) :
                Lean.Compiler.LCNF.PP.M Lean.Format
                Instances For
                  source
                  def Lean.Compiler.LCNF.PP.ppLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) :
                  Lean.Compiler.LCNF.PP.M Lean.Format
                  Instances For
                    source
                    def Lean.Compiler.LCNF.PP.getFunType (ps : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) :
                    Lean.CoreM Lean.Expr
                    Instances For
                      source
                      partial def Lean.Compiler.LCNF.PP.ppFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) :
                      Lean.Compiler.LCNF.PP.M Lean.Format
                      source
                      partial def Lean.Compiler.LCNF.PP.ppAlt (alt : Lean.Compiler.LCNF.Alt) :
                      Lean.Compiler.LCNF.PP.M Lean.Format
                      source
                      partial def Lean.Compiler.LCNF.PP.ppCode (c : Lean.Compiler.LCNF.Code) :
                      Lean.Compiler.LCNF.PP.M Lean.Format
                      source
                      def Lean.Compiler.LCNF.PP.run {α : Type} (x : Lean.Compiler.LCNF.PP.M α) :
                      Lean.Compiler.LCNF.CompilerM α
                      Instances For
                        source
                        def Lean.Compiler.LCNF.ppCode (code : Lean.Compiler.LCNF.Code) :
                        Lean.Compiler.LCNF.CompilerM Lean.Format
                        Instances For
                          source
                          def Lean.Compiler.LCNF.ppLetValue (e : Lean.Compiler.LCNF.LetValue) :
                          Lean.Compiler.LCNF.CompilerM Lean.Format
                          Instances For
                            source
                            def Lean.Compiler.LCNF.ppDecl (decl : Lean.Compiler.LCNF.Decl) :
                            Lean.Compiler.LCNF.CompilerM Lean.Format
                            Instances For
                              source
                              def Lean.Compiler.LCNF.ppFunDecl (decl : Lean.Compiler.LCNF.FunDecl) :
                              Lean.Compiler.LCNF.CompilerM Lean.Format
                              Instances For
                                source
                                def Lean.Compiler.LCNF.runCompilerWithoutModifyingState {α : Type} (x : Lean.Compiler.LCNF.CompilerM α) :
                                Lean.CoreM α

                                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.

                                Instances For
                                  source
                                  def Lean.Compiler.LCNF.ppDecl' (decl : Lean.Compiler.LCNF.Decl) :
                                  Lean.CoreM Lean.Format

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

                                  Instances For
                                    source
                                    def Lean.Compiler.LCNF.ppCode' (code : Lean.Compiler.LCNF.Code) :
                                    Lean.CoreM Lean.Format

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

                                    Instances For