Documentation

Lean.Expr

inductive Lean.Literal :

Literal values for Expr.

Instances For

    Total order on Expr literal values. Natural number values are smaller than string literal values.

    Equations
    Instances For
      Equations

      Arguments in forallE binders can be labelled as implicit or explicit.

      Each lam or forallE binder comes with a binderInfo argument (stored in ExprData). This can be set to

      • default -- (x : α)
      • implicit -- {x : α}
      • strict_implicit -- ⦃x : α⦄
      • inst_implicit -- [x : α].
      • aux_decl -- Auxiliary definitions are helper methods that Lean generates. aux_decl is used for _match, _fun_match, _let_match and the self reference that appears in recursive pattern matching.

      The difference between implicit {} and strict-implicit ⦃⦄ is how implicit arguments are treated that are not followed by explicit arguments. {} arguments are applied eagerly, while ⦃⦄ arguments are left partially applied:

      def foo {x : Nat} : Nat := x
      def bar ⦃x : Nat⦄ : Nat := x
      #check foo -- foo : Nat
      #check bar -- bar : ⦃x : Nat⦄ → Nat
      

      See also the Lean manual.

      Instances For

        Return true if the given BinderInfo does not correspond to an implicit binder annotation (i.e., implicit, strictImplicit, or instImplicit).

        Equations
        Instances For

          Return true if the given BinderInfo is an instance implicit annotation (e.g., [Decidable α])

          Equations
          Instances For

            Return true if the given BinderInfo is a regular implicit annotation (e.g., {α : Type u})

            Equations
            Instances For

              Return true if the given BinderInfo is a strict implicit annotation (e.g., {{α : Type u}})

              Equations
              Instances For
                @[reducible, inline]

                Expression metadata. Used with the Expr.mdata constructor.

                Equations
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For

                    Cached hash code, cached results, and other data for Expr.

                    • hash : 32-bits
                    • approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions
                    • hasFVar : 1-bit -- does it contain free variables?
                    • hasExprMVar : 1-bit -- does it contain metavariables?
                    • hasLevelMVar : 1-bit -- does it contain level metavariables?
                    • hasLevelParam : 1-bit -- does it contain level parameters?
                    • looseBVarRange : 20-bits

                    Remark: this is mostly an internal datastructure used to implement Expr, most will never have to use it.

                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  Equations
                                  Instances For
                                    @[extern lean_uint8_to_uint64]
                                    Equations
                                    Instances For
                                      def Lean.Expr.mkData (h : UInt64) (looseBVarRange : optParam Nat 0) (approxDepth : optParam UInt32 0) (hasFVar : optParam Bool false) (hasExprMVar : optParam Bool false) (hasLevelMVar : optParam Bool false) (hasLevelParam : optParam Bool false) :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[inline]

                                        Optimized version of Expr.mkData for applications.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[inline]
                                          def Lean.Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar : Bool) (hasExprMVar : Bool) (hasLevelMVar : Bool) (hasLevelParam : Bool) :
                                          Equations
                                          Instances For
                                            @[inline]
                                            def Lean.Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar : Bool) (hasExprMVar : Bool) (hasLevelMVar : Bool) (hasLevelParam : Bool) :
                                            Equations
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              structure Lean.FVarId :

                                              The unique free variable identifier. It is just a hierarchical name, but we wrap it in FVarId to make sure they don't get mixed up with MVarId.

                                              This is not the user-facing name for a free variable. This information is stored in the local context (LocalContext). The unique identifiers are generated using a NameGenerator.

                                              Instances For
                                                Equations
                                                Equations

                                                A set of unique free variable identifiers. This is a persistent data structure implemented using red-black trees.

                                                Equations
                                                Instances For
                                                  Equations
                                                  Equations
                                                  Instances For

                                                    A set of unique free variable identifiers implemented using hashtables. Hashtables are faster than red-black trees if they are used linearly. They are not persistent data-structures.

                                                    Equations
                                                    Instances For

                                                      A mapping from free variable identifiers to values of type α. This is a persistent data structure implemented using red-black trees.

                                                      Equations
                                                      Instances For
                                                        def Lean.FVarIdMap.insert {α : Type} (s : Lean.FVarIdMap α) (fvarId : Lean.FVarId) (a : α) :
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          Equations
                                                          • Lean.instInhabitedFVarIdMap = { default := }
                                                          structure Lean.MVarId :

                                                          Universe metavariable Id

                                                          Instances For
                                                            Equations
                                                            Equations
                                                            Equations
                                                            Instances For
                                                              Equations
                                                              Instances For
                                                                Equations
                                                                Equations
                                                                Instances For
                                                                  def Lean.MVarIdMap.insert {α : Type} (s : Lean.MVarIdMap α) (mvarId : Lean.MVarId) (a : α) :
                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    instance Lean.instForInMVarIdMapProdMVarId {m : Type u_1 → Type u_2} {α : Type} :
                                                                    Equations
                                                                    Equations
                                                                    • Lean.instInhabitedMVarIdMap = { default := }
                                                                    @[extern lean_expr_data]
                                                                    noncomputable def Lean.Expr.data :
                                                                    Equations
                                                                    Instances For
                                                                      inductive Lean.Expr :

                                                                      Lean expressions. This data structure is used in the kernel and elaborator. However, expressions sent to the kernel should not contain metavariables.

                                                                      Remark: we use the E suffix (short for Expr) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use.

                                                                      • bvar: NatLean.Expr

                                                                        The bvar constructor represents bound variables, i.e. occurrences of a variable in the expression where there is a variable binder above it (i.e. introduced by a lam, forallE, or letE).

                                                                        The deBruijnIndex parameter is the de-Bruijn index for the bound variable. See the Wikipedia page on de-Bruijn indices for additional information.

                                                                        For example, consider the expression fun x : Nat => forall y : Nat, x = y. The x and y variables in the equality expression are constructed using bvar and bound to the binders introduced by the earlier lam and forallE constructors. Here is the corresponding Expr representation for the same expression:

                                                                        .lam `x (.const `Nat [])
                                                                          (.forallE `y (.const `Nat [])
                                                                            (.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0))
                                                                            .default)
                                                                          .default
                                                                        
                                                                      • fvar: Lean.FVarIdLean.Expr

                                                                        The fvar constructor represent free variables. These free variable occurrences are not bound by an earlier lam, forallE, or letE constructor and its binder exists in a local context only.

                                                                        Note that Lean uses the locally nameless approach. See McBride and McKinna for additional details.

                                                                        When "visiting" the body of a binding expression (i.e. lam, forallE, or letE), bound variables are converted into free variables using a unique identifier, and their user-facing name, type, value (for LetE), and binder annotation are stored in the LocalContext.

                                                                      • mvar: Lean.MVarIdLean.Expr

                                                                        Metavariables are used to represent "holes" in expressions, and goals in the tactic framework. Metavariable declarations are stored in the MetavarContext. Metavariables are used during elaboration, and are not allowed in the kernel, or in the code generator.

                                                                      • sort: Lean.LevelLean.Expr

                                                                        Used for Type u, Sort u, and Prop:

                                                                        • Prop is represented as .sort .zero,
                                                                        • Sort u as .sort (.param `u), and
                                                                        • Type u as .sort (.succ (.param `u))
                                                                      • const: Lake.NameList Lean.LevelLean.Expr

                                                                        A (universe polymorphic) constant that has been defined earlier in the module or by another imported module. For example, @Eq.{1} is represented as Expr.const `Eq [.succ .zero], and @Array.map.{0, 0} is represented as Expr.const `Array.map [.zero, .zero].

                                                                      • app: Lean.ExprLean.ExprLean.Expr

                                                                        A function application.

                                                                        For example, the natural number one, i.e. Nat.succ Nat.zero is represented as Expr.app (.const `Nat.succ []) (.const .zero []). Note that multiple arguments are represented using partial application.

                                                                        For example, the two argument application f x y is represented as Expr.app (.app f x) y.

                                                                      • lam: Lake.NameLean.ExprLean.ExprLean.BinderInfoLean.Expr

                                                                        A lambda abstraction (aka anonymous functions). It introduces a new binder for variable x in scope for the lambda body.

                                                                        For example, the expression fun x : Nat => x is represented as

                                                                        Expr.lam `x (.const `Nat []) (.bvar 0) .default
                                                                        
                                                                      • forallE: Lake.NameLean.ExprLean.ExprLean.BinderInfoLean.Expr

                                                                        A dependent arrow (a : α) → β) (aka forall-expression) where β may dependent on a. Note that this constructor is also used to represent non-dependent arrows where β does not depend on a.

                                                                        For example:

                                                                      • letE: Lake.NameLean.ExprLean.ExprLean.ExprBoolLean.Expr

                                                                        Let-expressions.

                                                                        IMPORTANT: The nonDep flag is for "local" use only. That is, a module should not "trust" its value for any purpose. In the intended use-case, the compiler will set this flag, and be responsible for maintaining it. Other modules may not preserve its value while applying transformations.

                                                                        Given an environment, a metavariable context, and a local context, we say a let-expression let x : t := v; e is non-dependent when it is equivalent to (fun x : t => e) v. In contrast, the dependent let-expression let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b is type correct, but (fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2 is not.

                                                                        The let-expression let x : Nat := 2; Nat.succ x is represented as

                                                                        Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
                                                                        
                                                                      • lit: Lean.LiteralLean.Expr

                                                                        Natural number and string literal values.

                                                                        They are not really needed, but provide a more compact representation in memory for these two kinds of literals, and are used to implement efficient reduction in the elaborator and kernel. The "raw" natural number 2 can be represented as Expr.lit (.natVal 2). Note that, it is definitionally equal to:

                                                                        Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
                                                                        
                                                                      • mdata: Lean.MDataLean.ExprLean.Expr

                                                                        Metadata (aka annotations).

                                                                        We use annotations to provide hints to the pretty-printer, store references to Syntax nodes, position information, and save information for elaboration procedures (e.g., we use the inaccessible annotation during elaboration to mark Exprs that correspond to inaccessible patterns).

                                                                        Note that Expr.mdata data e is definitionally equal to e.

                                                                      • proj: Lake.NameNatLean.ExprLean.Expr

                                                                        Projection-expressions. They are redundant, but are used to create more compact terms, speedup reduction, and implement eta for structures. The type of struct must be an structure-like inductive type. That is, it has only one constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators check whether the typeName matches the type of struct, and whether the (zero-based) index is valid (i.e., it is smaller than the number of constructor fields). When exporting Lean developments to other systems, proj can be replaced with typeName.rec applications.

                                                                        Example, given a : Nat × Bool, a.1 is represented as

                                                                        .proj `Prod 0 a
                                                                        
                                                                      Instances For

                                                                        The constructor name for the given expression. This is used for debugging purposes.

                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          • e.hash = e.data.hash
                                                                          Instances For

                                                                            Return true if e contains free variables. This is a constant time operation.

                                                                            Equations
                                                                            • e.hasFVar = e.data.hasFVar
                                                                            Instances For

                                                                              Return true if e contains expression metavariables. This is a constant time operation.

                                                                              Equations
                                                                              • e.hasExprMVar = e.data.hasExprMVar
                                                                              Instances For

                                                                                Return true if e contains universe (aka Level) metavariables. This is a constant time operation.

                                                                                Equations
                                                                                • e.hasLevelMVar = e.data.hasLevelMVar
                                                                                Instances For

                                                                                  Does the expression contain level (aka universe) or expression metavariables? This is a constant time operation.

                                                                                  Equations
                                                                                  • e.hasMVar = (e.data.hasExprMVar || e.data.hasLevelMVar)
                                                                                  Instances For

                                                                                    Return true if e contains universe level parameters. This is a constant time operation.

                                                                                    Equations
                                                                                    • e.hasLevelParam = e.data.hasLevelParam
                                                                                    Instances For

                                                                                      Return the approximated depth of an expression. This information is used to compute the expression hash code, and speedup comparisons. This is a constant time operation. We say it is approximate because it maxes out at 255.

                                                                                      Equations
                                                                                      • e.approxDepth = e.data.approxDepth.toUInt32
                                                                                      Instances For

                                                                                        The range of de-Bruijn variables that are loose. That is, bvars that are not bound by a binder. For example, bvar i has range i + 1 and an expression with no loose bvars has range 0.

                                                                                        Equations
                                                                                        • e.looseBVarRange = e.data.looseBVarRange.toNat
                                                                                        Instances For

                                                                                          Return the binder information if e is a lambda or forall expression, and .default otherwise.

                                                                                          Equations
                                                                                          Instances For

                                                                                            Export functions.

                                                                                            @[export lean_expr_hash]
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[export lean_expr_has_fvar]
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[export lean_expr_has_expr_mvar]
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[export lean_expr_has_level_mvar]
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[export lean_expr_has_mvar]
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[export lean_expr_has_level_param]
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[export lean_expr_loose_bvar_range]
                                                                                                        Equations
                                                                                                        • e.looseBVarRangeEx = e.data.looseBVarRange
                                                                                                        Instances For
                                                                                                          @[export lean_expr_binder_info]
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def Lean.mkConst (declName : Lake.Name) (us : optParam (List Lean.Level) []) :

                                                                                                            mkConst declName us return .const declName us.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Return the type of a literal value.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[export lean_lit_type]
                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  .bvar idx is now the preferred form.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    .sort u is now the preferred form.

                                                                                                                    Equations
                                                                                                                    Instances For

                                                                                                                      .fvar fvarId is now the preferred form. This function is seldom used, free variables are often automatically created using the telescope functions (e.g., forallTelescope and lambdaTelescope) at MetaM.

                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        .mvar mvarId is now the preferred form. This function is seldom used, metavariables are often created using functions such as mkFresheExprMVar at MetaM.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          .mdata m e is now the preferred form.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def Lean.mkProj (structName : Lake.Name) (idx : Nat) (struct : Lean.Expr) :

                                                                                                                            .proj structName idx struct is now the preferred form.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[match_pattern]

                                                                                                                              .app f a is now the preferred form.

                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                .lam x t b bi is now the preferred form.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  .forallE x t b bi is now the preferred form.

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    Return fun (_ : Unit), e

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      def Lean.mkLet (x : Lake.Name) (t : Lean.Expr) (v : Lean.Expr) (b : Lean.Expr) (nonDep : optParam Bool false) :

                                                                                                                                      .letE x t v b nonDep is now the preferred form.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[match_pattern]
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[match_pattern]
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            @[match_pattern]
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[match_pattern]
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[match_pattern]
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[match_pattern]
                                                                                                                                                  def Lean.mkApp6 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) :
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[match_pattern]
                                                                                                                                                    def Lean.mkApp7 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) :
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[match_pattern]
                                                                                                                                                      def Lean.mkApp8 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) (e₄ : Lean.Expr) :
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[match_pattern]
                                                                                                                                                        def Lean.mkApp9 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) (e₄ : Lean.Expr) (e₅ : Lean.Expr) :
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[match_pattern]
                                                                                                                                                          def Lean.mkApp10 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) (e₄ : Lean.Expr) (e₅ : Lean.Expr) (e₆ : Lean.Expr) :
                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            .lit l is now the preferred form.

                                                                                                                                                            Equations
                                                                                                                                                            Instances For

                                                                                                                                                              Return the "raw" natural number .lit (.natVal n). This is not the default representation used by the Lean frontend. See mkNatLit.

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                Return a natural number literal used in the frontend. It is a OfNat.ofNat application. Recall that all theorems and definitions containing numeric literals are encoded using OfNat.ofNat applications in the frontend.

                                                                                                                                                                Equations
                                                                                                                                                                Instances For

                                                                                                                                                                  Return the string literal .lit (.strVal s)

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[export lean_expr_mk_bvar]
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[export lean_expr_mk_fvar]
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[export lean_expr_mk_mvar]
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[export lean_expr_mk_sort]
                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[export lean_expr_mk_const]
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[export lean_expr_mk_app]
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[export lean_expr_mk_lambda]
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[export lean_expr_mk_forall]
                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[export lean_expr_mk_let]
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[export lean_expr_mk_lit]
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[export lean_expr_mk_mdata]
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[export lean_expr_mk_proj]
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            mkAppN f #[a₀, ..., aₙ] constructs the application f a₀ a₁ ... aₙ.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              def Lean.mkAppRange (f : Lean.Expr) (i : Nat) (j : Nat) (args : Array Lean.Expr) :

                                                                                                                                                                                              mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ] ==> the expression f a_i ... a_{j-1}

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Same as mkApp f args but reversing args.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[extern lean_expr_dbg_to_string]
                                                                                                                                                                                                  @[extern lean_expr_quick_lt]

                                                                                                                                                                                                  A total order for expressions. We say it is quick because it first compares the hashcodes.

                                                                                                                                                                                                  @[extern lean_expr_lt]
                                                                                                                                                                                                  opaque Lean.Expr.lt (a : Lean.Expr) (b : Lean.Expr) :

                                                                                                                                                                                                  A total order for expressions that takes the structure into account (e.g., variable names).

                                                                                                                                                                                                  @[extern lean_expr_eqv]

                                                                                                                                                                                                  Return true iff a and b are alpha equivalent. Binder annotations are ignored.

                                                                                                                                                                                                  @[extern lean_expr_equal]

                                                                                                                                                                                                  Return true iff a and b are equal. Binder names and annotations are taken into account.

                                                                                                                                                                                                  Return true if the given expression is a .sort ..

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    Return true if the given expression is of the form .sort (.succ ..).

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      Return true if the given expression is of the form .sort (.succ .zero).

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                        Return true if the given expression is .sort .zero

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                          Return true if the given expression is a bound variable.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                            Return true if the given expression is a metavariable.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              Return true if the given expression is a free variable.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                Return true if the given expression is an application.

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                  Return true if the given expression is a projection .proj ..

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                    Return true if the given expression is a constant.

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                      Return true if the given expression is a constant of the given name. Examples:

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                        Return true if the given expression is a free variable with the given id. Examples:

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                          Return true if the given expression is a forall-expression aka (dependent) arrow.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                            Return true if the given expression is a lambda abstraction aka anonymous function.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                              Return true if the given expression is a forall or lambda expression.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                Return true if the given expression is a let-expression.

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                  Return true if the given expression is a metadata.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                    Return true if the given expression is a literal value.

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • (fn.app arg).appFn! = fn
                                                                                                                                                                                                                                      • x.appFn! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!" 893 15 "application expected"
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • (fn.app arg).appArg! = arg
                                                                                                                                                                                                                                        • x.appArg! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!" 897 15 "application expected"
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              def Lean.Expr.appArg (e : Lean.Expr) (h : e.isApp = true) :
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • (fn.app a).appArg x = a
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                def Lean.Expr.appFn (e : Lean.Expr) (h : e.isApp = true) :
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                • (fn.app a).appFn x = fn
                                                                                                                                                                                                                                                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

                                                                                                                                                                                                                                                                  If the expression is a constant, return that name. Otherwise return Name.anonymous.

                                                                                                                                                                                                                                                                  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
                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                    Return the "body" of a forall expression. Example: let e be the representation for forall (p : Prop) (q : Prop), p ∧ q, then getForallBody e returns .app (.app (.const `And []) (.bvar 1)) (.bvar 0)

                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    • (Lean.Expr.forallE binderName binderType body binderInfo).getForallBody = body.getForallBody
                                                                                                                                                                                                                                                                                                    • x.getForallBody = x
                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                      Given a sequence of nested foralls (a₁ : α₁) → ... → (aₙ : αₙ) → _, returns the names [a₁, ... aₙ].

                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      • (Lean.Expr.forallE binderName binderType body binderInfo).getForallBinderNames = binderName :: body.getForallBinderNames
                                                                                                                                                                                                                                                                                                      • x.getForallBinderNames = []
                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                        If the given expression is a sequence of function applications f a₁ .. aₙ, return f. Otherwise return the input expression.

                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        • (fn.app arg).getAppFn = fn.getAppFn
                                                                                                                                                                                                                                                                                                        • x.getAppFn = x
                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                          Similar to getAppFn, but skips mdata

                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                          • (f.app arg).getAppFn' = f.getAppFn'
                                                                                                                                                                                                                                                                                                          • (Lean.Expr.mdata data a).getAppFn' = a.getAppFn'
                                                                                                                                                                                                                                                                                                          • x.getAppFn' = x
                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                            Given f a₀ a₁ ... aₙ, returns true if f is a constant with name n.

                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                              Given f a₁ ... aᵢ, returns true if f is a constant with name n and has the correct number of arguments.

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              • (Lean.Expr.const c us).isAppOfArity x 0 = (c == x)
                                                                                                                                                                                                                                                                                                              • (f.app arg).isAppOfArity x a.succ = f.isAppOfArity x a
                                                                                                                                                                                                                                                                                                              • x✝¹.isAppOfArity x✝ x = false
                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                Similar to isAppOfArity but skips Expr.mdata.

                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                • (Lean.Expr.mdata data b).isAppOfArity' x✝ x = b.isAppOfArity' x✝ x
                                                                                                                                                                                                                                                                                                                • (Lean.Expr.const c us).isAppOfArity' x 0 = (c == x)
                                                                                                                                                                                                                                                                                                                • (f.app arg).isAppOfArity' x a.succ = f.isAppOfArity' x a
                                                                                                                                                                                                                                                                                                                • x✝¹.isAppOfArity' x✝ x = false
                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                  Counts the number n of arguments for an expression f a₁ .. aₙ.

                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                    Like Lean.Expr.getAppFn but assumes the application has up to maxArgs arguments. If there are any more arguments than this, then they are returned by getAppFn as part of the function.

                                                                                                                                                                                                                                                                                                                    In particular, if the given expression is a sequence of function applications f a₁ .. aₙ, returns f a₁ .. aₖ where k is minimal such that n - k ≤ maxArgs.

                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      @[inline]

                                                                                                                                                                                                                                                                                                                      Given f a₁ a₂ ... aₙ, returns #[a₁, ..., aₙ]

                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                        @[inline]

                                                                                                                                                                                                                                                                                                                        Like Lean.Expr.getAppArgs but returns up to maxArgs arguments.

                                                                                                                                                                                                                                                                                                                        In particular, given f a₁ a₂ ... aₙ, returns #[aₖ₊₁, ..., aₙ] where k is minimal such that the size of this array is at most maxArgs.

                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                          @[inline]

                                                                                                                                                                                                                                                                                                                          Same as getAppArgs but reverse the output array.

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                            @[specialize #[]]
                                                                                                                                                                                                                                                                                                                            def Lean.Expr.withAppAux {α : Sort u_1} (k : Lean.ExprArray Lean.Exprα) :
                                                                                                                                                                                                                                                                                                                            Lean.ExprArray Lean.ExprNatα
                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                              def Lean.Expr.withApp {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
                                                                                                                                                                                                                                                                                                                              α

                                                                                                                                                                                                                                                                                                                              Given e = f a₁ a₂ ... aₙ, returns k f #[a₁, ..., aₙ].

                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                Return the function (name) and arguments of an application.

                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  @[inline]

                                                                                                                                                                                                                                                                                                                                  Given f a_1 ... a_n, returns #[a_1, ..., a_n]. Note that f may be an application. The resulting array has size n even if f.getAppNumArgs < n.

                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                      Given e of the form f a_1 ... a_n, return f. If n is greater than the number of arguments, then return e.getAppFn.

                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                        Given e of the form f a_1 ... a_n ... a_m, return f a_1 ... a_n. If n is greater than the arity, then return e.

                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                        • e.getAppPrefix n = e.stripArgsN (e.getAppNumArgs - n)
                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                          def Lean.Expr.traverseApp {M : TypeType u_1} [Monad M] (f : Lean.ExprM Lean.Expr) (e : Lean.Expr) :

                                                                                                                                                                                                                                                                                                                                          Given e = fn a₁ ... aₙ, runs f on fn and each of the arguments aᵢ and makes a new function application with the results.

                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                            def Lean.Expr.withAppRev {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
                                                                                                                                                                                                                                                                                                                                            α

                                                                                                                                                                                                                                                                                                                                            Same as withApp but with arguments reversed.

                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                              • (fn.app a).getRevArgD 0 x = a
                                                                                                                                                                                                                                                                                                                                              • (f.app arg).getRevArgD i.succ x = f.getRevArgD i x
                                                                                                                                                                                                                                                                                                                                              • x✝¹.getRevArgD x✝ x = x
                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                • (fn.app a).getRevArg! 0 = a
                                                                                                                                                                                                                                                                                                                                                • (f.app arg).getRevArg! i.succ = f.getRevArg! i
                                                                                                                                                                                                                                                                                                                                                • x✝.getRevArg! x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!" 1199 20 "invalid index"
                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                  Similar to getRevArg! but skips mdata

                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                  • (Lean.Expr.mdata data a).getRevArg!' x = a.getRevArg!' x
                                                                                                                                                                                                                                                                                                                                                  • (fn.app a).getRevArg!' 0 = a
                                                                                                                                                                                                                                                                                                                                                  • (f.app arg).getRevArg!' i.succ = f.getRevArg!' i
                                                                                                                                                                                                                                                                                                                                                  • x✝.getRevArg!' x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!'" 1206 20 "invalid index"
                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                    def Lean.Expr.getArg! (e : Lean.Expr) (i : Nat) (n : optParam Nat e.getAppNumArgs) :

                                                                                                                                                                                                                                                                                                                                                    Given f a₀ a₁ ... aₙ, returns the ith argument or panics if out of bounds.

                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                    • e.getArg! i n = e.getRevArg! (n - i - 1)
                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                                                      def Lean.Expr.getArg!' (e : Lean.Expr) (i : Nat) (n : optParam Nat e.getAppNumArgs) :

                                                                                                                                                                                                                                                                                                                                                      Similar to getArg!, but skips mdata

                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                      • e.getArg!' i n = e.getRevArg!' (n - i - 1)
                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                        def Lean.Expr.getArgD (e : Lean.Expr) (i : Nat) (v₀ : Lean.Expr) (n : optParam Nat e.getAppNumArgs) :

                                                                                                                                                                                                                                                                                                                                                        Given f a₀ a₁ ... aₙ, returns the ith argument or returns v₀ if out of bounds.

                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                        • e.getArgD i v₀ n = e.getRevArgD (n - i - 1) v₀
                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                          • e.hasLooseBVars = decide (e.looseBVarRange > 0)
                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                            Return true if e is a non-dependent arrow. Remark: the following function assumes e does not have loose bound variables.

                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                              @[extern lean_expr_has_loose_bvar]
                                                                                                                                                                                                                                                                                                                                                              opaque Lean.Expr.hasLooseBVar (e : Lean.Expr) (bvarIdx : Nat) :

                                                                                                                                                                                                                                                                                                                                                              Return true if e contains the loose bound variable bvarIdx in an explicit parameter, or in the range if tryRange == true.

                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                              • (Lean.Expr.forallE binderName d b bi).hasLooseBVarInExplicitDomain x✝ x = (bi.isExplicit && d.hasLooseBVar x✝ || b.hasLooseBVarInExplicitDomain (x✝ + 1) x)
                                                                                                                                                                                                                                                                                                                                                              • x✝¹.hasLooseBVarInExplicitDomain x✝ x = (x && x✝¹.hasLooseBVar x✝)
                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                @[extern lean_expr_lower_loose_bvars]

                                                                                                                                                                                                                                                                                                                                                                Lower the loose bound variables >= s in e by d. That is, a loose bound variable bvar i with i >= s is mapped to bvar (i-d).

                                                                                                                                                                                                                                                                                                                                                                Remark: if s < d, then the result is e.

                                                                                                                                                                                                                                                                                                                                                                @[extern lean_expr_lift_loose_bvars]

                                                                                                                                                                                                                                                                                                                                                                Lift loose bound variables >= s in e by d.

                                                                                                                                                                                                                                                                                                                                                                inferImplicit e numParams considerRange updates the first numParams parameter binder annotations of the e forall type. It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or the resulting type if considerRange == true.

                                                                                                                                                                                                                                                                                                                                                                Remark: we use this function to infer the bind annotations of inductive datatype constructors, and structure projections. When the {} annotation is used in these commands, we set considerRange == false.

                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_instantiate]

                                                                                                                                                                                                                                                                                                                                                                  Instantiates the loose bound variables in e using the subst array, where a loose Expr.bvar i at "binding depth" d is instantiated with subst[i - d] if 0 <= i - d < subst.size, and otherwise it is replaced with Expr.bvar (i - subst.size); non-loose bound variables are not touched.

                                                                                                                                                                                                                                                                                                                                                                  If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, then conceptually instantiate is instantiating the last n of these and reindexing the remaining ones. Warning: instantiate uses the de Bruijn indexing to index the subst array, which might be the reverse order from what you might expect. See also Lean.Expr.instantiateRev.

                                                                                                                                                                                                                                                                                                                                                                  Terminology. The "binding depth" of a subexpression is the number of bound variables available to that subexpression by virtue of being in the bodies of Expr.forallE, Expr.lam, and Expr.letE expressions. A bound variable Expr.bvar i is "loose" if its de Bruijn index i is not less than its binding depth.)

                                                                                                                                                                                                                                                                                                                                                                  About instantiation. Instantiation isn't mere substitution. When an expression from subst is being instantiated, its internal loose bound variables have their de Bruijn indices incremented by the binding depth of the replaced loose bound variable. This is necessary for the substituted expression to still refer to the correct binders after instantiation. Similarly, the reason loose bound variables not instantiated using subst have their de Bruijn indices decremented like Expr.bvar (i - subst.size) is that instantiate can be used to eliminate binding expressions internal to a larger expression, and this adjustment keeps these bound variables referring to the same binders.

                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_instantiate1]

                                                                                                                                                                                                                                                                                                                                                                  Instantiates loose bound variable 0 in e using the expression subst, where in particular a loose Expr.bvar i at binding depth d is instantiated with subst if i = d, and otherwise it is replaced with Expr.bvar (i - 1); non-loose bound variables are not touched.

                                                                                                                                                                                                                                                                                                                                                                  If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, then conceptually instantiate1 is instantiating the last one of these and reindexing the remaining ones.

                                                                                                                                                                                                                                                                                                                                                                  This function is equivalent to instantiate e #[subst], but it avoids allocating an array.

                                                                                                                                                                                                                                                                                                                                                                  See the documentation for Lean.Expr.instantiate for a description of instantiation. In short, during instantiation the loose bound variables in subst have their own de Bruijn indices updated to account for the binding depth of the replaced loose bound variable.

                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_instantiate_rev]

                                                                                                                                                                                                                                                                                                                                                                  Instantiates the loose bound variables in e using the subst array. This is equivalent to Lean.Expr.instantiate e subst.reverse, but it avoids reversing the array. In particular, rather than instantiating Expr.bvar i with subst[i - d] it instantiates with subst[subst.size - 1 - (i - d)], where d is the binding depth.

                                                                                                                                                                                                                                                                                                                                                                  This function instantiates with the "forwards" indexing scheme. For example, if e represents the expression fun x y => x + y, then instantiateRev e.bindingBody!.bindingBody! #[a, b] yields a + b. The instantiate function on the other hand would yield b + a, since de Bruijn indices count outwards.

                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_instantiate_range]
                                                                                                                                                                                                                                                                                                                                                                  opaque Lean.Expr.instantiateRange (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (subst : Array Lean.Expr) :

                                                                                                                                                                                                                                                                                                                                                                  Similar to Lean.Expr.instantiate, but considers only the substitutions subst in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= subst.size does not hold.

                                                                                                                                                                                                                                                                                                                                                                  This function is equivalent to instantiate e (subst.extract beginIdx endIdx), but it does not allocate a new array.

                                                                                                                                                                                                                                                                                                                                                                  This instantiates with the "backwards" indexing scheme. See also Lean.Expr.instantiateRevRange, which instantiates with the "forwards" indexing scheme.

                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_instantiate_rev_range]
                                                                                                                                                                                                                                                                                                                                                                  opaque Lean.Expr.instantiateRevRange (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (subst : Array Lean.Expr) :

                                                                                                                                                                                                                                                                                                                                                                  Similar to Lean.Expr.instantiateRev, but considers only the substitutions subst in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= subst.size does not hold.

                                                                                                                                                                                                                                                                                                                                                                  This function is equivalent to instantiateRev e (subst.extract beginIdx endIdx), but it does not allocate a new array.

                                                                                                                                                                                                                                                                                                                                                                  This instantiates with the "forwards" indexing scheme (see the docstring for Lean.Expr.instantiateRev for an example). See also Lean.Expr.instantiateRange, which instantiates with the "backwards" indexing scheme.

                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_abstract]

                                                                                                                                                                                                                                                                                                                                                                  Replace free (or meta) variables xs with loose bound variables.

                                                                                                                                                                                                                                                                                                                                                                  @[extern lean_expr_abstract_range]

                                                                                                                                                                                                                                                                                                                                                                  Similar to abstract, but consider only the first min n xs.size entries in xs.

                                                                                                                                                                                                                                                                                                                                                                  Replace occurrences of the free variable fvar in e with v

                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                  • e.replaceFVar fvar v = (e.abstract #[fvar]).instantiate1 v
                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                    Replace occurrences of the free variable fvarId in e with v

                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                    • e.replaceFVarId fvarId v = e.replaceFVar (Lean.mkFVar fvarId) v
                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                      Replace occurrences of the free variables fvars in e with vs

                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                      • e.replaceFVars fvars vs = (e.abstract fvars).instantiateRev vs
                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                        Returns true when the expression does not have any sub-expressions.

                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                              abbrev Lean.ExprMap (α : Type) :
                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                  abbrev Lean.SExprMap (α : Type) :
                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                    @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                          Auxiliary type for forcing == to be structural equality for Expr

                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                            • { val := e₁ }.beq { val := e₂ } = e₁.equal e₂
                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                              • { val := e }.hash = e.hash
                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                    def Lean.Expr.mkAppRevRange (f : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (revArgs : Array Lean.Expr) :

                                                                                                                                                                                                                                                                                                                                                                                                    mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)

                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                      def Lean.Expr.betaRev (f : Lean.Expr) (revArgs : Array Lean.Expr) (useZeta : optParam Bool false) (preserveMData : optParam Bool false) :

                                                                                                                                                                                                                                                                                                                                                                                                      If f is a lambda expression, than "beta-reduce" it using revArgs. This function is often used with getAppRev or withAppRev. Examples:

                                                                                                                                                                                                                                                                                                                                                                                                      • betaRev (fun x y => t x y) #[] ==> fun x y => t x y
                                                                                                                                                                                                                                                                                                                                                                                                      • betaRev (fun x y => t x y) #[a] ==> fun y => t a y
                                                                                                                                                                                                                                                                                                                                                                                                      • betaRev (fun x y => t x y) #[a, b] ==> t b a
                                                                                                                                                                                                                                                                                                                                                                                                      • betaRev (fun x y => t x y) #[a, b, c, d] ==> t d c b a Suppose t is (fun x y => t x y) a b c d, then args := t.getAppRev is #[d, c, b, a], and betaRev (fun x y => t x y) #[d, c, b, a] is t a b c d.

                                                                                                                                                                                                                                                                                                                                                                                                      If useZeta is true, the function also performs zeta-reduction (reduction of let binders) to create further opportunities for beta reduction.

                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                      • f.betaRev revArgs useZeta preserveMData = if (revArgs.size == 0) = true then f else let sz := revArgs.size; Lean.Expr.betaRev.go revArgs useZeta preserveMData sz f 0
                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                        partial def Lean.Expr.betaRev.go (revArgs : Array Lean.Expr) (useZeta : optParam Bool false) (preserveMData : optParam Bool false) (sz : Nat) (e : Lean.Expr) (i : Nat) :

                                                                                                                                                                                                                                                                                                                                                                                                        Apply the given arguments to f, beta-reducing if f is a lambda expression. See docstring for betaRev for examples.

                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                        • f.beta args = f.betaRev args.reverse
                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                          Count the number of lambdas at the head of the given expression.

                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                          • (Lean.Expr.lam binderName binderType b binderInfo).getNumHeadLambdas = b.getNumHeadLambdas + 1
                                                                                                                                                                                                                                                                                                                                                                                                          • (Lean.Expr.mdata data b).getNumHeadLambdas = b.getNumHeadLambdas
                                                                                                                                                                                                                                                                                                                                                                                                          • x.getNumHeadLambdas = 0
                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                            Return true if the given expression is the function of an expression that is target for (head) beta reduction. If useZeta = true, then let-expressions are visited. That is, it assumes that zeta-reduction (aka let-expansion) is going to be used.

                                                                                                                                                                                                                                                                                                                                                                                                            See isHeadBetaTarget.

                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                              (fun x => e) a ==> e[x/a].

                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                Return true if the given expression is a target for (head) beta reduction. If useZeta = true, then let-expressions are visited. That is, it assumes that zeta-reduction (aka let-expansion) is going to be used.

                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                  If e is of the form (fun x₁ ... xₙ => f x₁ ... xₙ) and f does not contain x₁, ..., xₙ, then return some f. Otherwise, return none.

                                                                                                                                                                                                                                                                                                                                                                                                                  It assumes e does not have loose bound variables.

                                                                                                                                                                                                                                                                                                                                                                                                                  Remark: may be 0

                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                    Similar to etaExpanded?, but only succeeds if ₙ ≥ 1.

                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                      Return some e' if e is of the form optParam _ e'

                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                      • e.getOptParamDefault? = if e.isAppOfArity `optParam 2 = true then some e.appArg! else none
                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                        Return some e' if e is of the form autoParam _ e'

                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                        • e.getAutoParamTactic? = if e.isAppOfArity `autoParam 2 = true then some e.appArg! else none
                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                          @[export lean_is_out_param]

                                                                                                                                                                                                                                                                                                                                                                                                                          Return true if e is of the form outParam _

                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                          • e.isOutParam = e.isAppOfArity `outParam 1
                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                            Return true if e is of the form semiOutParam _

                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                            • e.isSemiOutParam = e.isAppOfArity `semiOutParam 1
                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                              Return true if e is of the form optParam _ _

                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                              • e.isOptParam = e.isAppOfArity `optParam 2
                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                Return true if e is of the form autoParam _ _

                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                • e.isAutoParam = e.isAppOfArity `autoParam 2
                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                  @[export lean_expr_consume_type_annotations]

                                                                                                                                                                                                                                                                                                                                                                                                                                  Remove outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

                                                                                                                                                                                                                                                                                                                                                                                                                                  Remove metadata annotations and outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

                                                                                                                                                                                                                                                                                                                                                                                                                                  Similar to appFn, but also applies cleanupAnnotations to resulting function. This function is used compile the match_expr term.

                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                  • (fn.app a).appFnCleanup x = fn.cleanupAnnotations
                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                    • e.isFalse = e.cleanupAnnotations.isConstOf `False
                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                      • e.isTrue = e.cleanupAnnotations.isConstOf `True
                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                        Checks if an expression is a "natural number numeral in normal form", i.e. of type Nat, and explicitly of the form OfNat.ofNat n where n matches .lit (.natVal n) for some literal natural number n. and if so returns n.

                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                          Checks if an expression is an "integer numeral in normal form", i.e. of type Nat or Int, and either a natural number numeral in normal form (as specified by nat?), or the negation of a positive natural number numberal in normal form, and if so returns the integer.

                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                            @[inline]

                                                                                                                                                                                                                                                                                                                                                                                                                                            Return true iff e contains a free variable which satisfies p.

                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                              @[specialize #[]]
                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                Return true if e contains the given free variable.

                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                • e.containsFVar fvarId = e.hasAnyFVar fun (x : Lean.FVarId) => x == fvarId
                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                  The update functions try to avoid allocating new values using pointer equality. Note that if the update*! functions are used under a match-expression, the compiler will eliminate the double-match.

                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateApp!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                  • (fn.app arg).updateApp! newFn newArg = Lean.mkApp newFn newArg
                                                                                                                                                                                                                                                                                                                                                                                                                                                  • e.updateApp! newFn newArg = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateApp!" 1674 15 "application expected"
                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                      @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateConst!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                        @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateSort!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                          @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateMData!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                            @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateProj!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                              @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateForall!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                              def Lean.Expr.updateForall! (e : Lean.Expr) (newBinfo : Lean.BinderInfo) (newDomain : Lean.Expr) (newBody : Lean.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                              • (Lean.Expr.forallE binderName binderType body binderInfo).updateForall! newBinfo newDomain newBody = Lean.mkForall binderName newBinfo newDomain newBody
                                                                                                                                                                                                                                                                                                                                                                                                                                                              • e.updateForall! newBinfo newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateForall!" 1738 23 "forall expected"
                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                def Lean.Expr.updateForallE! (e : Lean.Expr) (newDomain : Lean.Expr) (newBody : Lean.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                • (Lean.Expr.forallE binderName binderType body binderInfo).updateForallE! newDomain newBody = (Lean.Expr.forallE binderName binderType body binderInfo).updateForall! binderInfo newDomain newBody
                                                                                                                                                                                                                                                                                                                                                                                                                                                                • e.updateForallE! newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateForallE!" 1743 24 "forall expected"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLambda!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  def Lean.Expr.updateLambda! (e : Lean.Expr) (newBinfo : Lean.BinderInfo) (newDomain : Lean.Expr) (newBody : Lean.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • (Lean.Expr.lam binderName binderType body binderInfo).updateLambda! newBinfo newDomain newBody = Lean.mkLambda binderName newBinfo newDomain newBody
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • e.updateLambda! newBinfo newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateLambda!" 1758 19 "lambda expected"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    def Lean.Expr.updateLambdaE! (e : Lean.Expr) (newDomain : Lean.Expr) (newBody : Lean.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • (Lean.Expr.lam binderName binderType body binderInfo).updateLambdaE! newDomain newBody = (Lean.Expr.lam binderName binderType body binderInfo).updateLambda! binderInfo newDomain newBody
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • e.updateLambdaE! newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateLambdaE!" 1763 20 "lambda expected"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      @[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLet!Impl]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      def Lean.Expr.updateLet! (e : Lean.Expr) (newType : Lean.Expr) (newVal : Lean.Expr) (newBody : Lean.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • (Lean.Expr.letE declName type value body nonDep).updateLet! newType newVal newBody = Lean.Expr.letE declName newType newVal newBody nonDep
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • e.updateLet! newType newVal newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateLet!" 1778 22 "let expression expected"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • (f.app a).updateFn x = (f.app a).updateApp! (f.updateFn x) a
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • x✝.updateFn x = x
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          partial def Lean.Expr.eta (e : Lean.Expr) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Eta reduction. If e is of the form (fun x => f x), then return f.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          def Lean.Expr.setOption {α : Type} (e : Lean.Expr) (optionName : Lake.Name) [Lean.KVMap.Value α] (val : α) :

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Annotate e with the given option. The information is stored using metadata around e.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Annotate e with pp.explicit := flag The delaborator uses pp options.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • e.setPPExplicit flag = e.setOption `pp.explicit flag
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Annotate e with pp.universes := flag The delaborator uses pp options.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              • e.setPPUniverses flag = e.setOption `pp.universes flag
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                If e is an application f a_1 ... a_n annotate f, a_1 ... a_n with pp.explicit := false, and annotate e with pp.explicit := true.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                • e.setAppPPExplicit = e
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Similar for setAppPPExplicit, but only annotate children with pp.explicit := false if e does not contain metavariables.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • e.setAppPPExplicitForExposingMVars = e
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Returns true if e is a let_fun expression, which is an expression of the form letFun v f. Ideally f is a lambda, but we do not require that here. Warning: if the let_fun is applied to additional arguments (such as in (let_fun f := id; id) 1), this function returns false.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • e.isLetFun = e.isAppOfArity `letFun 4
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Recognizes a let_fun expression. For let_fun n : t := v; b, returns some (n, t, v, b), which are the first four arguments to Lean.Expr.letE. Warning: if the let_fun is applied to additional arguments (such as in (let_fun f := id; id) 1), this function returns none.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      let_fun expressions are encoded as letFun v (fun (n : t) => b). They can be created using Lean.Meta.mkLetFun.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      If in the encoding of let_fun the last argument to letFun is eta reduced, this returns Name.anonymous for the binder name.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Like Lean.Expr.letFun?, but handles the case when the let_fun expression is possibly applied to additional arguments. Returns those arguments in addition to the values returned by letFun?.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          @[specialize #[]]

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Maps f on each immediate child of the given expression.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            def Lean.Expr.foldlM {α : Type} {m : TypeType u_1} [Monad m] (f : αLean.Exprm α) (init : α) (e : Lean.Expr) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            m α

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            e.foldlM f a folds the monadic function f over the subterms of the expression e, with initial value a.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Returns the size of e as a tree, i.e. nodes reachable via multiple paths are counted multiple times.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              This is a naive implementation that visits shared subterms multiple times instead of caching their sizes. It is primarily meant for debugging.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Annotate e with the given annotation name kind. It uses metadata to store the annotation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Return some e' if e = mkAnnotation kind e'

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Auxiliary annotation used to mark terms marked with the "inaccessible" annotation .(t) and _ in patterns.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Return some e' if e = mkInaccessible e'.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        During elaboration expressions corresponding to pattern matching terms are annotated with Syntax objects. This function returns some (stx, p') if p is the pattern p' annotated with stx

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Annotate the pattern p with stx. This is an auxiliary annotation for producing better hover information.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Return some p if e is an annotated pattern (inaccessible? or patternWithRef?)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Annotate e with the LHS annotation. The delaborator displays expressions of the form lhs = rhs as lhs when they have this annotation. This is used to implement the infoview for the conv mode.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              This version of mkLHSGoal does not check that the argument is an equality.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Return some lhs if e = mkLHSGoal e', where e' is of the form lhs = rhs.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Polymorphic operation for generating unique/fresh free variable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • Lean.mkFreshFVarId = do let __do_liftLean.mkFreshId pure { name := __do_lift }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Polymorphic operation for generating unique/fresh metavariable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    • Lean.mkFreshMVarId = do let __do_liftLean.mkFreshId pure { name := __do_lift }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Polymorphic operation for generating unique/fresh universe metavariable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • Lean.mkFreshLMVarId = do let __do_liftLean.mkFreshId pure { name := __do_lift }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Return Not p

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Return p ∨ q

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Return p ∧ q

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Make an n-ary And application. mkAndN [] returns True.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Return Classical.em p

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Return p ↔ q

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Constants for Nat typeclasses.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Given a : Nat, returns Nat.succ a

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Given a b : Nat, returns a + b

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Given a b : Nat, returns a - b

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Given a b : Nat, returns a * b

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Given a b : Nat, return a ≤ b

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Given a b : Nat, return a = b

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For