Documentation

Lean.Compiler.LCNF.InferType

Type inference for LCNF #

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.InferType.InferTypeM (α : Type) :
Type

We use a regular local context to store temporary local declarations created during type inference.

Equations
Instances For
    source
    def Lean.Compiler.LCNF.InferType.getBinderName (fvarId : Lean.FVarId) :
    Lean.Compiler.LCNF.InferType.InferTypeM Lean.Name
    Instances For
      source
      def Lean.Compiler.LCNF.InferType.getType (fvarId : Lean.FVarId) :
      Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Compiler.LCNF.InferType.mkForallFVars (xs : Array Lean.Expr) (type : Lean.Expr) :
        Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
        Instances For
          source
          def Lean.Compiler.LCNF.InferType.mkForallParams (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) :
          Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[inline]
            def Lean.Compiler.LCNF.InferType.withLocalDecl {α : Type} (binderName : Lean.Name) (type : Lean.Expr) (binderInfo : Lean.BinderInfo) (k : Lean.Expr → Lean.Compiler.LCNF.InferType.InferTypeM α) :
            Lean.Compiler.LCNF.InferType.InferTypeM α
            Instances For
              source
              def Lean.Compiler.LCNF.InferType.inferConstType (declName : Lean.Name) (us : List Lean.Level) :
              Lean.Compiler.LCNF.CompilerM Lean.Expr
              Instances For
                source
                def Lean.Compiler.LCNF.InferType.inferLitValueType (value : Lean.Compiler.LCNF.LitValue) :
                Lean.Expr
                Instances For
                  source
                  def Lean.Compiler.LCNF.InferType.inferArgType (arg : Lean.Compiler.LCNF.Arg) :
                  Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                  Equations
                  Instances For
                    source
                    partial def Lean.Compiler.LCNF.InferType.inferType (e : Lean.Expr) :
                    Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                    source
                    def Lean.Compiler.LCNF.InferType.inferLetValueType (e : Lean.Compiler.LCNF.LetValue) :
                    Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                    Instances For
                      source
                      def Lean.Compiler.LCNF.InferType.inferAppTypeCore (fType : Lean.Expr) (args : Array Lean.Compiler.LCNF.Arg) :
                      Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        partial def Lean.Compiler.LCNF.InferType.inferAppType (e : Lean.Expr) :
                        Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                        source
                        def Lean.Compiler.LCNF.InferType.inferProjType (structName : Lean.Name) (idx : Nat) (s : Lean.FVarId) :
                        Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          partial def Lean.Compiler.LCNF.InferType.getLevel? (type : Lean.Expr) :
                          Lean.Compiler.LCNF.InferType.InferTypeM (Option Lean.Level)
                          source
                          partial def Lean.Compiler.LCNF.InferType.inferForallType (e : Lean.Expr) :
                          Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                          source
                          partial def Lean.Compiler.LCNF.InferType.inferForallType.go (e : Lean.Expr) (fvars : Array Lean.Expr) :
                          Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                          source
                          partial def Lean.Compiler.LCNF.InferType.inferLambdaType (e : Lean.Expr) :
                          Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                          source
                          partial def Lean.Compiler.LCNF.InferType.inferLambdaType.go (e : Lean.Expr) (fvars all : Array Lean.Expr) :
                          Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
                          source
                          def Lean.Compiler.LCNF.inferType (e : Lean.Expr) :
                          Lean.Compiler.LCNF.CompilerM Lean.Expr
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def Lean.Compiler.LCNF.inferAppType (fnType : Lean.Expr) (args : Array Lean.Compiler.LCNF.Arg) :
                            Lean.Compiler.LCNF.CompilerM Lean.Expr
                            Instances For
                              source
                              def Lean.Compiler.LCNF.getLevel (type : Lean.Expr) :
                              Lean.Compiler.LCNF.CompilerM Lean.Level
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def Lean.Compiler.LCNF.Arg.inferType (arg : Lean.Compiler.LCNF.Arg) :
                                Lean.Compiler.LCNF.CompilerM Lean.Expr
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def Lean.Compiler.LCNF.LetValue.inferType (e : Lean.Compiler.LCNF.LetValue) :
                                  Lean.Compiler.LCNF.CompilerM Lean.Expr
                                  Instances For
                                    source
                                    def Lean.Compiler.LCNF.Code.inferType (code : Lean.Compiler.LCNF.Code) :
                                    Lean.Compiler.LCNF.CompilerM Lean.Expr
                                    Instances For
                                      source
                                      def Lean.Compiler.LCNF.Code.inferParamType (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) :
                                      Lean.Compiler.LCNF.CompilerM Lean.Expr
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        def Lean.Compiler.LCNF.AltCore.inferType (alt : Lean.Compiler.LCNF.Alt) :
                                        Lean.Compiler.LCNF.CompilerM Lean.Expr
                                        Instances For
                                          source
                                          def Lean.Compiler.LCNF.mkAuxLetDecl (e : Lean.Compiler.LCNF.LetValue) (prefixName : Lean.Name := `_x) :
                                          Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def Lean.Compiler.LCNF.mkForallParams (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) :
                                            Lean.Compiler.LCNF.CompilerM Lean.Expr
                                            Instances For
                                              source
                                              def Lean.Compiler.LCNF.mkAuxFunDecl (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : Lean.Name := `_f) :
                                              Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
                                              Instances For
                                                source
                                                def Lean.Compiler.LCNF.mkAuxJpDecl (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : Lean.Name := `_jp) :
                                                Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
                                                Instances For
                                                  source
                                                  def Lean.Compiler.LCNF.mkAuxJpDecl' (param : Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : Lean.Name := `_jp) :
                                                  Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
                                                  Equations
                                                  Instances For
                                                    source
                                                    def Lean.Compiler.LCNF.mkCasesResultType (alts : Array Lean.Compiler.LCNF.Alt) :
                                                    Lean.Compiler.LCNF.CompilerM Lean.Expr
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      def Lean.Compiler.LCNF.isErasedCompatible (type : Lean.Expr) (predVars : Array Bool := #[]) :
                                                      Lean.Compiler.LCNF.CompilerM Bool

                                                      Return true if type should be erased. See item 1 in the note above where x ◾ ◾ is a proposition and should be erased when the universe level parameter is set to 0.

                                                      Remark: predVars is a bitmask that indicates whether de-bruijn variables are predicates or not. That is, #i is a predicate if predVars[predVars.size - i - 1] = true

                                                      Instances For
                                                        source
                                                        partial def Lean.Compiler.LCNF.isErasedCompatible.go (type : Lean.Expr) (predVars : Array Bool) :
                                                        Lean.Compiler.LCNF.CompilerM Bool
                                                        source
                                                        partial def Lean.Compiler.LCNF.eqvTypes (a b : Lean.Expr) :
                                                        Bool

                                                        Return true if the given LCNF are equivalent. List Nat and (fun x => List x) Nat are both equivalent.