Documentation

Lean.Meta.InferType

def Lean.Expr.instantiateBetaRevRange (e : Expr) (start stop : Nat) (args : Array Expr) :

Auxiliary function for instantiating the loose bound variables in e with args[start:stop]. This function is similar to instantiateRevRange, but it applies beta-reduction when we instantiate a bound variable with a lambda expression. Example: Given the term #0 a, and start := 0, stop := 1, args := #[fun x => x] the result is a instead of (fun x => x) a. This reduction is useful when we are inferring the type of eliminator-like applications. For example, given (n m : Nat) (f : Nat → Nat) (h : m = n), the type of Eq.subst (motive := fun x => f m = f x) h rfl is motive n which is (fun (x : Nat) => f m = f x) n This function reduces the new application to f m = f n

We use it to implement inferAppType

Equations
    Instances For
      Equations
        Instances For
          def Lean.Meta.throwIncorrectNumberOfLevels {α : Type} (constName : Name) (us : List Level) :
          Equations
            Instances For
              def Lean.Meta.throwTypeExcepted {α : Type} (type : Expr) :
              Equations
                Instances For
                  Equations
                    Instances For
                      def Lean.Meta.throwUnknownMVar {α : Type} (mvarId : MVarId) :
                      Equations
                        Instances For
                          @[inline]

                          Ensure MetaM configuration is strong enough for inferring/checking types. For example, beta := true is essential when type checking.

                          Remark: we previously use the default configuration here, but this is problematic because it overrides unrelated configurations.

                          Equations
                            Instances For
                              @[export lean_infer_type]
                              Equations
                                Instances For
                                  Equations
                                    Instances For

                                      isPropQuick e is an "approximate" predicate which returns LBool.true if e is a proposition.

                                      isProp e returns true if e is a proposition.

                                      If e contains metavariables, it may not be possible to decide whether is a proposition or not. We return false in this case. We considered using LBool and retuning LBool.undef, but we have no applications for it.

                                      Equations
                                        Instances For

                                          isProofQuick e is an "approximate" predicate which returns LBool.true if e is a proof.

                                          Equations
                                            Instances For

                                              isTypeQuick e is an "approximate" predicate which returns LBool.true if e is a type.

                                              Return true iff the type of e is a Sort _.

                                              Equations
                                                Instances For

                                                  Return u iff type is Sort u or As → Sort u.

                                                  Equations
                                                    Instances For

                                                      Return true iff type is Sort _ or As → Sort _.

                                                      Equations
                                                        Instances For

                                                          Return true iff type is Prop or As → Prop.

                                                          Equations
                                                            Instances For

                                                              Return true iff e : Sort _ or e : (forall As, Sort _). Remark: it subsumes isType

                                                              Equations
                                                                Instances For

                                                                  Given n and a non-dependent function type α₁ → α₂ → ... → αₙ → Sort u, returns the types α₁, α₂, ..., αₙ. Throws an error if there are not at least n argument types or if a later argument type depends on a prior one (i.e., it's a dependent function type).

                                                                  This can be used to infer the expected type of the alternatives when constructing a MatcherApp.

                                                                  Equations
                                                                    Instances For

                                                                      Infers the types of the next n parameters that e expects. See arrowDomainsN.

                                                                      Equations
                                                                        Instances For