Documentation

Lean.Meta.Basic

This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks. 1- Weak head normal form computation with support for metavariables and transparency modes. 2- Definitionally equality checking with support for metavariables (aka unification modulo definitional equality). 3- Type inference. 4- Type class resolution.

They are packed into the MetaM monad.

  • foApprox : Bool

    If foApprox is set to true, and some aᵢ is not a free variable, then we use first-order unification

      ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
    

    reduces to

      ?m a_1 ... a_i =?= f
      a_{i+1}        =?= b_1
      ...
      a_{i+k}        =?= b_k
    
  • ctxApprox : Bool

    When ctxApprox is set to true, we relax condition 4, by creating an auxiliary metavariable ?n' with a smaller context than ?m'.

  • quasiPatternApprox : Bool

    When quasiPatternApprox is set to true, we ignore condition 2.

  • constApprox : Bool

    When constApprox is set to true, we solve ?m t =?= c using ?m := fun _ => c when ?m t is not a higher-order pattern and c is not an application as

  • isDefEqStuckEx : Bool

    When the following flag is set, isDefEq throws the exeption Exeption.isDefEqStuck whenever it encounters a constraint ?m ... =?= t where ?m is read only. This feature is useful for type class resolution where we may want to notify the caller that the TC problem may be solveable later after it assigns ?m.

  • Controls which definitions and theorems can be unfolded by isDefEq and whnf.

  • zetaNonDep : Bool

    If zetaNonDep == false, then non dependent let-decls are not zeta expanded.

  • trackZeta : Bool

    When trackZeta == true, we store zetaFVarIds all free variables that have been zeta-expanded.

  • unificationHints : Bool

    Enable/disable the unification hints feature.

  • proofIrrelevance : Bool

    Enables proof irrelevance at isDefEq

  • assignSyntheticOpaque : Bool

    By default synthetic opaque metavariables are not assigned by isDefEq. Motivation: we want to make sure typing constraints resolved during elaboration should not "fill" holes that are supposed to be filled using tactics. However, this restriction is too restrictive for tactics such as exact t. When elaborating t, we dot not fill named holes when solving typing constraints or TC resolution. But, we ignore the restriction when we try to unify the type of t with the goal target type. We claim this is not a hack and is defensible behavior because this last unification step is not really part of the term elaboration.

  • offsetCnstrs : Bool

    Enable/Disable support for offset constraints such as ?x + 1 =?= e

  • Eta for structures configuration mode.

Configuration flags for the MetaM monad. Many of them are used to control the isDefEq function that checks whether two terms are definitionally equal or not. Recall that when isDefEq is trying to check whether ?m@C a₁ ... aₙ and t are definitionally equal (?m@C a₁ ... aₙ =?= t), where ?m@C as a shorthand for C |- ?m : t where t is the type of ?m. We solve it using the assignment ?m := fun a₁ ... aₙ => t if

  1. a₁ ... aₙ are pairwise distinct free variables that are ​not​ let-variables.
  2. a₁ ... aₙ are not in C
  3. t only contains free variables in C and/or {a₁, ..., aₙ}
  4. For every metavariable ?m'@C' occurring in t, C' is a subprefix of C
  5. ?m does not occur in t
Instances For
    • binderInfo : Lean.BinderInfo

      The binder annotation for the parameter.

    • hasFwdDeps : Bool

      hasFwdDeps is true if there is another parameter whose type depends on this one.

    • backDeps : Array Nat

      backDeps contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on.

    • isProp : Bool

      isProp is true if the parameter is always a proposition.

    • isDecInst : Bool

      isDecInst is true if the parameter's type is of the form Decidable .... This information affects the generation of congruence theorems.

    • higherOrderOutParam : Bool

      higherOrderOutParam is true if this parameter is a higher-order output parameter of local instance. Example:

      getElem :
        {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
        {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
        (xs : cont) → (i : idx) → dom xs i → elem
      

      This flag is true for the parameter dom because it is output parameter of [self : GetElem cont idx elem dom]

    • dependsOnHigherOrderOutParam : Bool

      dependsOnHigherOrderOutParam is true if the type of this parameter depends on the higher-order output parameter of a previous local instance. Example:

      getElem :
        {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
        {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
        (xs : cont) → (i : idx) → dom xs i → elem
      

      This flag is true for the parameter with type dom xs i since dom is an output parameter of the instance [self : GetElem cont idx elem dom]

    Function parameter information cache.

    Instances For
      • Parameter information cache.

      • resultDeps : Array Nat

        resultDeps contains the function result type backwards dependencies. That is, the (0-indexed) position of parameters that the result type depends on.

      Function information cache. See ParamInfo.

      Instances For
        • The transparency mode used to compute the FunInfo.

        • expr : Lean.Expr

          The function being cached information about. It is quite often an Expr.const.

        • nargs? : Option Nat

          nargs? = some n if the cached information was computed assuming the function has arity n. If nargs? = none, then the cache information consumed the arrow type as much as possible unsing the current transparency setting. X

        Key for the function information cache.

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

                  A mapping (s, t) ↦ isDefEq s t. TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache). We should also investigate the impact on memory consumption.

                  Instances For

                    Cache datastructures for type inference, type class resolution, whnf, and definitional equality.

                    Instances For

                      "Context" for a postponed universe constraint. lhs and rhs are the surrounding isDefEq call when the postponed constraint was created.

                      Instances For

                        Auxiliary structure for representing postponed universe constraints. Remark: the fields ref and rootDefEq? are used for error message generation only. Remark: we may consider improving the error message generation in the future.

                        Instances For

                          MetaM monad state.

                          Instances For

                            Backtrackable state for the MetaM monad.

                            Instances For

                              Contextual information for the MetaM monad.

                              Instances For
                                @[inline, reducible]
                                abbrev Lean.Meta.MetaM (α : Type) :
                                Instances For

                                  Restore backtrackable parts of the state.

                                  Instances For
                                    @[inline]
                                    def Lean.Meta.MetaM.run {α : Type} (x : Lean.MetaM α) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := , postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :
                                    Instances For
                                      @[inline]
                                      def Lean.Meta.MetaM.run' {α : Type} (x : Lean.MetaM α) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := , postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :
                                      Instances For
                                        @[inline]
                                        def Lean.Meta.MetaM.toIO {α : Type} (x : Lean.MetaM α) (ctxCore : Lean.Core.Context) (sCore : Lean.Core.State) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := , postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :
                                        Instances For
                                          @[inline]
                                          def Lean.Meta.liftMetaM {m : TypeType u_1} {α : Type} [MonadLiftT Lean.MetaM m] (x : Lean.MetaM α) :
                                          m α
                                          Instances For
                                            @[inline]
                                            def Lean.Meta.mapMetaM {m : TypeType u_1} [MonadControlT Lean.MetaM m] [Monad m] (f : {α : Type} → Lean.MetaM αLean.MetaM α) {α : Type} (x : m α) :
                                            m α
                                            Instances For
                                              @[inline]
                                              def Lean.Meta.map1MetaM {m : TypeType u_1} {β : Sort u_2} [MonadControlT Lean.MetaM m] [Monad m] (f : {α : Type} → (βLean.MetaM α) → Lean.MetaM α) {α : Type} (k : βm α) :
                                              m α
                                              Instances For
                                                @[inline]
                                                def Lean.Meta.map2MetaM {m : TypeType u_1} {β : Sort u_2} {γ : Sort u_3} [MonadControlT Lean.MetaM m] [Monad m] (f : {α : Type} → (βγLean.MetaM α) → Lean.MetaM α) {α : Type} (k : βγm α) :
                                                m α
                                                Instances For

                                                  Return the array of postponed universe level constraints.

                                                  Instances For

                                                    Set the array of postponed universe level constraints.

                                                    Instances For
                                                      @[inline]

                                                      Modify the array of postponed universe level constraints.

                                                      Instances For

                                                        useEtaStruct inductName return true if we eta for structures is enabled for for the inductive datatype inductName.

                                                        Recall we have three different settings: .none (never use it), .all (always use it), .notClasses (enabled only for structure-like inductive types that are not classes).

                                                        The parameter inductName affects the result only if the current setting is .notClasses.

                                                        Instances For

                                                          WARNING: The following 4 constants are a hack for simulating forward declarations. They are defined later using the export attribute. This is hackish because we have to hard-code the true arity of these definitions here, and make sure the C names match. We have used another hack based on IO.Refs in the past, it was safer but less efficient.

                                                          @[extern 6 lean_whnf]

                                                          Reduces an expression to its Weak Head Normal Form. This is when the topmost expression has been fully reduced, but may contain subexpressions which have not been reduced.

                                                          @[extern 6 lean_infer_type]

                                                          Returns the inferred type of the given expression, or fails if it is not type-correct.

                                                          @[extern 7 lean_is_expr_def_eq]
                                                          @[extern 7 lean_is_level_def_eq]
                                                          @[extern 6 lean_synth_pending]
                                                          def Lean.Meta.withIncRecDepth {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                          n α
                                                          Instances For

                                                            Create a constant with the given name and new universe metavariables. Example: mkConstWithFreshMVarLevels `Monad returns @Monad.{?u, ?v}

                                                            Instances For

                                                              Return current transparency setting/mode.

                                                              Instances For

                                                                Return some mvarDecl where mvarDecl is mvarId declaration in the current metavariable context. Return none if mvarId has no declaration in the current metavariable context.

                                                                Instances For
                                                                  @[deprecated Lean.MVarId.findDecl?]
                                                                  Instances For

                                                                    Return mvarId declaration in the current metavariable context. Throw an exception if mvarId is not declarated in the current metavariable context.

                                                                    Instances For
                                                                      @[deprecated Lean.MVarId.getDecl]
                                                                      Instances For

                                                                        Return mvarId kind. Throw an exception if mvarId is not declarated in the current metavariable context.

                                                                        Instances For
                                                                          @[deprecated Lean.MVarId.getKind]
                                                                          Instances For

                                                                            Reture true if e is a synthetic (or synthetic opaque) metavariable

                                                                            Instances For

                                                                              Set mvarId kind in the current metavariable context.

                                                                              Instances For
                                                                                @[deprecated Lean.MVarId.setKind]
                                                                                Instances For

                                                                                  Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one

                                                                                  Instances For
                                                                                    @[deprecated Lean.MVarId.setType]
                                                                                    Instances For

                                                                                      Return true if the given metavariable is "read-only". That is, its depth is different from the current metavariable context depth.

                                                                                      Instances For
                                                                                        @[deprecated Lean.MVarId.isReadOnly]
                                                                                        Instances For

                                                                                          Return true if mvarId.isReadOnly return true or if mvarId is a synthetic opaque metavariable.

                                                                                          Recall isDefEq will not assign a value to mvarId if mvarId.isReadOnlyOrSyntheticOpaque.

                                                                                          Instances For
                                                                                            @[deprecated Lean.MVarId.isReadOnlyOrSyntheticOpaque]
                                                                                            Instances For

                                                                                              Return the level of the given universe level metavariable.

                                                                                              Instances For
                                                                                                @[deprecated Lean.LMVarId.getLevel]
                                                                                                Instances For

                                                                                                  Return true if the given universe metavariable is "read-only". That is, its depth is different from the current metavariable context depth.

                                                                                                  Instances For
                                                                                                    @[deprecated Lean.LMVarId.isReadOnly]
                                                                                                    Instances For

                                                                                                      Set the user-facing name for the given metavariable.

                                                                                                      Instances For
                                                                                                        @[deprecated Lean.MVarId.setUserName]
                                                                                                        Instances For

                                                                                                          Throw an exception saying fvarId is not declared in the current local context.

                                                                                                          Instances For
                                                                                                            @[deprecated Lean.FVarId.throwUnknown]
                                                                                                            Instances For

                                                                                                              Return some decl if fvarId is declared in the current local context.

                                                                                                              Instances For
                                                                                                                @[deprecated Lean.FVarId.findDecl?]
                                                                                                                Instances For

                                                                                                                  Return the local declaration for the given free variable. Throw an exception if local declaration is not in the current local context.

                                                                                                                  Instances For
                                                                                                                    @[deprecated Lean.FVarId.getDecl]
                                                                                                                    Instances For

                                                                                                                      Return the type of the given free variable.

                                                                                                                      Instances For

                                                                                                                        Return the binder information for the given free variable.

                                                                                                                        Instances For

                                                                                                                          Return some value if the given free variable is a let-declaration, and none otherwise.

                                                                                                                          Instances For

                                                                                                                            Return the user-facing name for the given free variable.

                                                                                                                            Instances For

                                                                                                                              Return true is the free variable is a let-variable.

                                                                                                                              Instances For

                                                                                                                                Get the local declaration associated to the given Expr in the current local context. Fails if the given expression is not a fvar or if no such declaration exists.

                                                                                                                                Instances For

                                                                                                                                  Given a user-facing name for a free variable, return its declaration in the current local context. Throw an exception if free variable is not declared.

                                                                                                                                  Instances For

                                                                                                                                    Given a user-facing name for a free variable, return the free variable or throw if not declared.

                                                                                                                                    Instances For
                                                                                                                                      @[inline]

                                                                                                                                      Lift a MkBindingM monadic action x to MetaM.

                                                                                                                                      Instances For

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

                                                                                                                                        It is also similar to Expr.abstractRange, but handles metavariables correctly. It uses elimMVarDeps to ensure e and the type of the free variables xs do not contain a metavariable ?m s.t. local context of ?m contains a free variable in xs.

                                                                                                                                        Instances For
                                                                                                                                          @[deprecated Lean.Expr.abstractRangeM]
                                                                                                                                          Instances For

                                                                                                                                            Replace free (or meta) variables xs with loose bound variables. Similar to Expr.abstract, but handles metavariables correctly.

                                                                                                                                            Instances For
                                                                                                                                              @[deprecated Lean.Expr.abstractM]
                                                                                                                                              Instances For

                                                                                                                                                Collect forward dependencies for the free variables in toRevert. Recall that when reverting free variables xs, we must also revert their forward dependencies.

                                                                                                                                                Instances For

                                                                                                                                                  Takes an array xs of free variables or metavariables and a term e that may contain those variables, and abstracts and binds them as universal quantifiers.

                                                                                                                                                  • if usedOnly = true then only variables that the expression body depends on will appear.
                                                                                                                                                  • if usedLetOnly = true same as usedOnly except for let-bound variables. (That is, local constants which have been assigned a value.)
                                                                                                                                                  Instances For

                                                                                                                                                    Takes an array xs of free variables and metavariables and a body term e and creates fun ..xs => e, suitably abstracting e and the types in xs.

                                                                                                                                                    Instances For

                                                                                                                                                      fun _ : Unit => a

                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def Lean.Meta.withConfig {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (f : Lean.Meta.ConfigLean.Meta.Config) :
                                                                                                                                                        n αn α

                                                                                                                                                        withConfig f x executes x using the updated configuration object obtained by applying f.

                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Lean.Meta.withTrackingZeta {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                          n α
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]
                                                                                                                                                            def Lean.Meta.withoutProofIrrelevance {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                            n α
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              def Lean.Meta.withTransparency {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mode : Lean.Meta.TransparencyMode) :
                                                                                                                                                              n αn α
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                def Lean.Meta.withDefault {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                n α

                                                                                                                                                                withDefault x excutes x using the default transparency setting.

                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  def Lean.Meta.withReducible {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                  n α

                                                                                                                                                                  withReducible x excutes x using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def Lean.Meta.withReducibleAndInstances {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                    n α

                                                                                                                                                                    withReducibleAndInstances x excutes x using the .instances transparency setting. In this setting only definitions tagged as [reducible] or type class instances are unfolded.

                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]
                                                                                                                                                                      def Lean.Meta.withAtLeastTransparency {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mode : Lean.Meta.TransparencyMode) (x : n α) :
                                                                                                                                                                      n α

                                                                                                                                                                      Execute x ensuring the transparency setting is at least mode. Recall that .all > .default > .instances > .reducible.

                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        def Lean.Meta.withAssignableSyntheticOpaque {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                        n α

                                                                                                                                                                        Execute x allowing isDefEq to assign synthetic opaque metavariables.

                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          def Lean.Meta.savingCache {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} :
                                                                                                                                                                          n αn α
                                                                                                                                                                          Instances For
                                                                                                                                                                            def Lean.Meta.withNewLocalInstance {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (className : Lake.Name) (fvar : Lean.Expr) :
                                                                                                                                                                            n αn α

                                                                                                                                                                            Add entry { className := className, fvar := fvar } to localInstances, and then execute continuation k.

                                                                                                                                                                            Instances For

                                                                                                                                                                              isClass? type return some ClsName if type is an instance of the class ClsName. Example:

                                                                                                                                                                              #eval do
                                                                                                                                                                                let x ← mkAppM ``Inhabited #[mkConst ``Nat]
                                                                                                                                                                                IO.println (← isClass? x)
                                                                                                                                                                                -- (some Inhabited)
                                                                                                                                                                              
                                                                                                                                                                              Instances For
                                                                                                                                                                                def Lean.Meta.withNewLocalInstances {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (fvars : Array Lean.Expr) (j : Nat) :
                                                                                                                                                                                n αn α
                                                                                                                                                                                Instances For
                                                                                                                                                                                  def Lean.Meta.forallTelescope {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (type : Lean.Expr) (k : Array Lean.ExprLean.Exprn α) :
                                                                                                                                                                                  n α

                                                                                                                                                                                  Given type of the form forall xs, A, execute k xs A. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

                                                                                                                                                                                  Instances For
                                                                                                                                                                                    def Lean.Meta.forallTelescopeReducing {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (type : Lean.Expr) (k : Array Lean.ExprLean.Exprn α) :
                                                                                                                                                                                    n α

                                                                                                                                                                                    Similar to forallTelescope, but given type of the form forall xs, A, it reduces A and continues bulding the telescope if it is a forall.

                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def Lean.Meta.forallBoundedTelescope {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (type : Lean.Expr) (maxFVars? : Option Nat) (k : Array Lean.ExprLean.Exprn α) :
                                                                                                                                                                                      n α

                                                                                                                                                                                      Similar to forallTelescopeReducing, stops constructing the telescope when it reaches size maxFVars.

                                                                                                                                                                                      Instances For
                                                                                                                                                                                        def Lean.Meta.lambdaLetTelescope {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (e : Lean.Expr) (k : Array Lean.ExprLean.Exprn α) :
                                                                                                                                                                                        n α

                                                                                                                                                                                        Similar to lambdaTelescope but for lambda and let expressions.

                                                                                                                                                                                        Instances For
                                                                                                                                                                                          def Lean.Meta.lambdaTelescope {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (e : Lean.Expr) (k : Array Lean.ExprLean.Exprn α) :
                                                                                                                                                                                          n α

                                                                                                                                                                                          Given e of the form fun ..xs => A, execute k xs A. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Return the parameter names for the given global declaration.

                                                                                                                                                                                            Instances For

                                                                                                                                                                                              Given e of the form forall ..xs, A, this combinator will create a new metavariable for each x in xs and instantiate A with these. Returns a product containing

                                                                                                                                                                                              • the new metavariables
                                                                                                                                                                                              • the binder info for the xs
                                                                                                                                                                                              • the instantiated A
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Similar to forallMetaTelescope, but if e = forall ..xs, A it will reduce A to construct further mvars.

                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  Similar to forallMetaTelescopeReducing, stops constructing the telescope when it reaches size maxMVars.

                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    Similar to forallMetaTelescopeReducingAux but for lambda expressions.

                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      Create a free variable x with name, binderInfo and type, add it to the context and run in k. Then revert the context.

                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        def Lean.Meta.withLocalDeclD {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (name : Lake.Name) (type : Lean.Expr) (k : Lean.Exprn α) :
                                                                                                                                                                                                        n α
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          def Lean.Meta.withLocalDecls {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Lake.Name × Lean.BinderInfo × (Array Lean.Exprn Lean.Expr))) (k : Array Lean.Exprn α) :
                                                                                                                                                                                                          n α

                                                                                                                                                                                                          Append an array of free variables xs to the local context and execute k xs. declInfos takes the form of an array consisting of:

                                                                                                                                                                                                          • the name of the variable
                                                                                                                                                                                                          • the binder info of the variable
                                                                                                                                                                                                          • a type constructor for the variable, where the array consists of all of the free variables defined prior to this one. This is needed because the type of the variable may depend on prior variables.
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            partial def Lean.Meta.withLocalDecls.loop {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (declInfos : Array (Lake.Name × Lean.BinderInfo × (Array Lean.Exprn Lean.Expr))) (k : Array Lean.Exprn α) [Inhabited α] (acc : Array Lean.Expr) :
                                                                                                                                                                                                            n α
                                                                                                                                                                                                            def Lean.Meta.withLocalDeclsD {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Lake.Name × (Array Lean.Exprn Lean.Expr))) (k : Array Lean.Exprn α) :
                                                                                                                                                                                                            n α
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def Lean.Meta.withNewBinderInfos {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (bs : Array (Lean.FVarId × Lean.BinderInfo)) (k : n α) :
                                                                                                                                                                                                              n α
                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                Execute k using a local context where any x in xs that is tagged as instance implicit is treated as a regular implicit.

                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  def Lean.Meta.withLetDecl {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) (k : Lean.Exprn α) (kind : optParam Lean.LocalDeclKind Lean.LocalDeclKind.default) :
                                                                                                                                                                                                                  n α

                                                                                                                                                                                                                  Add the local declaration : := to the local context and execute k x, where x is a new free variable corresponding to the let-declaration. After executing k x, the local context is restored.

                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    def Lean.Meta.withLocalInstances {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (decls : List Lean.LocalDecl) :
                                                                                                                                                                                                                    n αn α

                                                                                                                                                                                                                    Register any local instance in decls

                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def Lean.Meta.withExistingLocalDecls {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (decls : List Lean.LocalDecl) :
                                                                                                                                                                                                                      n αn α

                                                                                                                                                                                                                      withExistingLocalDecls decls k, adds the given local declarations to the local context, and then executes k. This method assumes declarations in decls have valid FVarIds. After executing k, the local context is restored.

                                                                                                                                                                                                                      Remark: this method is used, for example, to implement the match-compiler. Each match-alternative commes with a local declarations (corresponding to pattern variables), and we use withExistingLocalDecls to add them to the local context before we process them.

                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        def Lean.Meta.withNewMCtxDepth {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (k : n α) (allowLevelAssignments : optParam Bool false) :
                                                                                                                                                                                                                        n α

                                                                                                                                                                                                                        withNewMCtxDepth k executes k with a higher metavariable context depth, where metavariables created outside the withNewMCtxDepth (with a lower depth) cannot be assigned. If allowLevelAssignments is set to true, then the level metavariable depth is not increased, and level metavariables from the outer scope can be assigned. (This is used by TC synthesis.)

                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          def Lean.Meta.withLCtx {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) :
                                                                                                                                                                                                                          n αn α

                                                                                                                                                                                                                          withLCtx lctx localInsts k replaces the local context and local instances, and then executes k. The local context and instances are restored after executing k. This method assumes that the local instances in localInsts are in the local context lctx.

                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            def Lean.MVarId.withContext {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mvarId : Lean.MVarId) :
                                                                                                                                                                                                                            n αn α

                                                                                                                                                                                                                            Execute x using the given metavariable LocalContext and LocalInstances. The type class resolution cache is flushed when executing x if its LocalInstances are different from the current ones.

                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[deprecated Lean.MVarId.withContext]
                                                                                                                                                                                                                              def Lean.Meta.withMVarContext {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mvarId : Lean.MVarId) :
                                                                                                                                                                                                                              n αn α
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                def Lean.Meta.withMCtx {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mctx : Lean.MetavarContext) :
                                                                                                                                                                                                                                n αn α

                                                                                                                                                                                                                                withMCtx mctx k replaces the metavariable context and then executes k. The metavariable context is restored after executing k.

                                                                                                                                                                                                                                This method is used to implement the type class resolution procedure.

                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                  def Lean.Meta.approxDefEq {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} :
                                                                                                                                                                                                                                  n αn α

                                                                                                                                                                                                                                  Execute x using approximate unification: foApprox, ctxApprox and quasiPatternApprox.

                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                    def Lean.Meta.fullApproxDefEq {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} :
                                                                                                                                                                                                                                    n αn α

                                                                                                                                                                                                                                    Similar to approxDefEq, but uses all available approximations. We don't use constApprox by default at approxDefEq because it often produces undesirable solution for monadic code. For example, suppose we have pure (x > 0) which has type ?m Prop. We also have the goal [Pure ?m]. Now, assume the expected type is IO Bool. Then, the unification constraint ?m Prop =?= IO Bool could be solved as ?m := fun _ => IO Bool using constApprox, but this spurious solution would generate a failure when we try to solve [Pure (fun _ => IO Bool)]

                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                      Instantiate assigned universe metavariables in u, and then normalize it.

                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                        whnf with reducible transparency.

                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                          whnf with default transparency.

                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                            whnf with instances transparency.

                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                              Mark declaration declName with the attribute [inline]. This method does not check whether the given declaration is a definition.

                                                                                                                                                                                                                                              Recall that this attribute can only be set in the same module where declName has been declared.

                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                Given e of the form forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return B[p_1, ..., p_n].

                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  Given e of the form fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return t[p_1, ..., p_n]. It uses whnf to reduce e if it is not a lambda

                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                    Pretty-print the given expression.

                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                      Pretty-print the given expression.

                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                        def Lean.Meta.orElse {α : Type} (x : Lean.MetaM α) (y : UnitLean.MetaM α) :
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                          def Lean.Meta.orelseMergeErrors {m : TypeType u_1} {α : Type} [MonadControlT Lean.MetaM m] [Monad m] (x : m α) (y : m α) (mergeRef : optParam (Lean.SyntaxLean.SyntaxLean.Syntax) fun r₁ x => r₁) (mergeMsg : optParam (Lean.MessageDataLean.MessageDataLean.MessageData) fun m₁ m₂ => m₁ ++ Lean.MessageData.ofFormat Lean.Format.line ++ Lean.MessageData.ofFormat Lean.Format.line ++ m₂) :
                                                                                                                                                                                                                                                          m α

                                                                                                                                                                                                                                                          Similar to orelse, but merge errors. Note that internal errors are not caught. The default mergeRef uses the ref (position information) for the first message. The default mergeMsg combines error messages using Format.line ++ Format.line as a separator.

                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                            Execute x, and apply f to the produced error message

                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                              def Lean.Meta.mapError {m : TypeType u_1} {α : Type} [MonadControlT Lean.MetaM m] [Monad m] (x : m α) (f : Lean.MessageDataLean.MessageData) :
                                                                                                                                                                                                                                                              m α
                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                Sort free variables using an order x < y iff x was defined before y. If a free variable is not in the local context, we use their id.

                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  Return true if declName is an inductive predicate. That is, inductive type in Prop.

                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    def Lean.Meta.processPostponed (mayPostpone : optParam Bool true) (exceptionOnFailure : optParam Bool false) :
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      partial def Lean.Meta.processPostponed.loop (mayPostpone : optParam Bool true) (exceptionOnFailure : optParam Bool false) :
                                                                                                                                                                                                                                                                      @[specialize #[]]

                                                                                                                                                                                                                                                                      checkpointDefEq x executes x and process all postponed universe level constraints produced by x. We keep the modifications only if processPostponed return true and x returned true.

                                                                                                                                                                                                                                                                      If mayPostpone == false, all new postponed universe level constraints must be solved before returning. We currently try to postpone universe constraints as much as possible, even when by postponing them we are not sure whether x really succeeded or not.

                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                        Determines whether two universe level expressions are definitionally equal to each other.

                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[inline, reducible]

                                                                                                                                                                                                                                                                          Determines whether two expressions are definitionally equal to each other.

                                                                                                                                                                                                                                                                          To control how metavariables are assigned and unified, metavariables and their context have a "depth". Given a metavariable ?m and a MetavarContext mctx, ?m is not assigned if ?m.depth != mctx.depth. The combinator withNewMCtxDepth x will bump the depth while executing x. So, withNewMCtxDepth (isDefEq a b) is isDefEq without any mvar assignment happening whereas isDefEq a b will assign any metavariables of the current depth in a and b to unify them.

                                                                                                                                                                                                                                                                          For matching (where only mvars in b should be assigned), we create the term inside the withNewMCtxDepth. For an example, see Lean.Meta.Simp.tryTheoremWithExtraArgs?

                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                            @[inline, reducible]

                                                                                                                                                                                                                                                                            Similar to isDefEq, but returns false if an exception has been thrown.

                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                              Eta expand the given expression. Example:

                                                                                                                                                                                                                                                                              etaExpand (mkConst ``Nat.add)
                                                                                                                                                                                                                                                                              

                                                                                                                                                                                                                                                                              produces fun x y => Nat.add x y

                                                                                                                                                                                                                                                                              Instances For