Documentation

Lean.Compiler.LCNF.PrettyPrinter

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.PP.M (α : Type) :
Type
Instances For
    source
    def Lean.Compiler.LCNF.PP.ppFVar (fvarId : FVarId) :
    M Format
    Instances For
      source
      def Lean.Compiler.LCNF.PP.ppExpr (e : Expr) :
      M Format
      Instances For
        source
        def Lean.Compiler.LCNF.PP.ppArg {pu : Purity} (e : Arg pu) :
        M Format
        Instances For
          source
          def Lean.Compiler.LCNF.PP.ppArgs {pu : Purity} (args : Array (Arg pu)) :
          M Format
          Instances For
            source
            def Lean.Compiler.LCNF.PP.ppLitValue (lit : LitValue) :
            M Format
            Instances For
              source
              @[implicit_reducible]
              instance Lean.Compiler.LCNF.PP.instToFormatCtorInfo :
              ToFormat CtorInfo
              source
              def Lean.Compiler.LCNF.PP.ppLetValue {pu : Purity} (e : LetValue pu) :
              M Format
              Instances For
                source
                def Lean.Compiler.LCNF.PP.ppParam {pu : Purity} (param : Param pu) :
                M Format
                Instances For
                  source
                  def Lean.Compiler.LCNF.PP.ppParams {pu : Purity} (params : Array (Param pu)) :
                  M Format
                  Instances For
                    source
                    def Lean.Compiler.LCNF.PP.ppLetDecl {pu : Purity} (letDecl : LetDecl pu) :
                    M Format
                    Instances For
                      source
                      def Lean.Compiler.LCNF.PP.getFunType {pu : Purity} (ps : Array (Param pu)) (type : Expr) :
                      CoreM Expr
                      Instances For
                        source
                        partial def Lean.Compiler.LCNF.PP.ppFunDecl {pu : Purity} (funDecl : FunDecl pu) :
                        M Format
                        source
                        partial def Lean.Compiler.LCNF.PP.ppAlt {pu : Purity} (alt : Alt pu) :
                        M Format
                        source
                        partial def Lean.Compiler.LCNF.PP.ppCode {pu : Purity} (c : Code pu) :
                        M Format
                        source
                        def Lean.Compiler.LCNF.PP.ppDeclValue {pu : Purity} (b : DeclValue pu) :
                        M Format
                        Instances For
                          source
                          def Lean.Compiler.LCNF.PP.run {α : Type} (x : M α) :
                          CompilerM α
                          Instances For
                            source
                            def Lean.Compiler.LCNF.ppCode {pu : Purity} (code : Code pu) :
                            CompilerM Format
                            Instances For
                              source
                              def Lean.Compiler.LCNF.ppLetValue {pu : Purity} (e : LetValue pu) :
                              CompilerM Format
                              Instances For
                                source
                                def Lean.Compiler.LCNF.ppDecl {pu : Purity} (decl : Decl pu) :
                                CompilerM Format
                                Instances For
                                  source
                                  def Lean.Compiler.LCNF.ppFunDecl {pu : Purity} (decl : FunDecl pu) :
                                  CompilerM Format
                                  Instances For
                                    source
                                    def Lean.Compiler.LCNF.runCompilerWithoutModifyingState {α : Type} (phase : Phase) (x : CompilerM α) :
                                    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' {pu : Purity} (decl : Decl pu) (phase : Phase) :
                                      CoreM 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' {pu : Purity} (code : Code pu) (phase : Phase) :
                                        CoreM Format

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

                                        Instances For