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.

Configuration for projection reduction. See whnfCore.

  • no: Lean.Meta.ProjReductionKind

    Projections s.i are not reduced at whnfCore.

  • yes: Lean.Meta.ProjReductionKind

    Projections s.i are reduced at whnfCore, and whnfCore is used at s during the process. Recall that whnfCore does not perform delta reduction (i.e., it will not unfold constant declarations).

  • yesWithDelta: Lean.Meta.ProjReductionKind

    Projections s.i are reduced at whnfCore, and whnf is used at s during the process. Recall that whnfCore does not perform delta reduction (i.e., it will not unfold constant declarations), but whnf does.

  • yesWithDeltaI: Lean.Meta.ProjReductionKind

    Projections s.i are reduced at whnfCore, and whnfAtMostI is used at s during the process. Recall that whnfAtMostI is like whnf but uses transparency at most instances. This option is stronger than yes, but weaker than yesWithDelta. We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations. When unifying e.g. (@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1, we only want to unify negation (and not all other field operations as well). Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986

Instances For

    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
    • 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 exception Exception.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 solvable later after it assigns ?m.

    • 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

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

    • trackZetaDelta : Bool

      When trackZetaDelta = true, we track all free variables that have been zetaDelta-expanded. That is, suppose the local context contains the declaration x : t := v, and we reduce x to v, then we insert x into State.zetaDeltaFVarIds. We use trackZetaDelta to discover which let-declarations let x := v; e can be represented as (fun x => e) v. When we find these declarations we set their nonDep flag with true. To find these let-declarations in a given term s, we 1- Reset State.zetaDeltaFVarIds 2- Set trackZetaDelta := true 3- Type-check s.

    • Eta for structures configuration mode.

    • univApprox : Bool

      When univApprox is set to true, we use approximations when solving postponed universe constraints. Examples:

      • max u ?v =?= u is solved with ?v := u and ignoring the solution ?v := 0.
      • max u w =?= mav u ?v is solved with ?v := w ignoring the solution ?v := max u w
    • iota : Bool

      If true, reduce recursor/matcher applications, e.g., Nat.rec true (fun _ _ => false) Nat.zero reduces to true

    • beta : Bool

      If true, reduce terms such as (fun x => t[x]) a into t[a]

    • Control projection reduction at whnfCore.

    • zeta : Bool

      Zeta reduction: let x := v; e[x] reduces to e[v]. We say a let-declaration let x := v; e is non dependent if it is equivalent to (fun x => e) v. Recall that

      fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
      

      is type correct, but

      fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
      

      is not.

    • zetaDelta : Bool

      Zeta-delta reduction: given a local context containing entry x : t := e, free variable x reduces to e.

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

      Configuration with key produced by Config.toKey.

      Instances For
        Equations
        Equations
        Instances For

          Function parameter information cache.

          • 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 type 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]

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

                    Function information cache. See ParamInfo.

                    • 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.

                    Instances For

                      Key for the function information cache.

                      • configKey : UInt64

                        key produced using Config.toKey.

                      • 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 using the current transparency setting. X

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

                          Resulting type for abstractMVars

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

                                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.

                                Equations
                                Instances For

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

                                  Instances For
                                    Equations
                                    • Lean.Meta.instInhabitedCache = { default := { inferType := default, funInfo := default, synthInstance := default, whnf := default, defEqTrans := default, defEqPerm := default } }

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

                                          MetaM monad state.

                                          Instances For
                                            Equations
                                            • Lean.Meta.instInhabitedState = { default := { mctx := default, cache := default, zetaDeltaFVarIds := default, postponed := default, diag := default } }

                                            Backtrackable state for the MetaM monad.

                                            Instances For

                                              Contextual information for the MetaM monad.

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

                                                The MetaM monad is a core component of Lean's metaprogramming framework, facilitating the construction and manipulation of expressions (Lean.Expr) within Lean.

                                                It builds on top of CoreM and additionally provides:

                                                • A LocalContext for managing free variables.
                                                • A MetavarContext for managing metavariables.
                                                • A Cache for caching results of the key MetaM operations.

                                                The key operations provided by MetaM are:

                                                • inferType, which attempts to automatically infer the type of a given expression.
                                                • whnf, which reduces an expression to the point where the outermost part is no longer reducible but the inside may still contain unreduced expression.
                                                • isDefEq, which determines whether two expressions are definitionally equal, possibly assigning meta variables in the process.
                                                • forallTelescope and lambdaTelescope, which make it possible to automatically move into (nested) binders while updating the local context.

                                                The following is a small example that demonstrates how to obtain and manipulate the type of a Fin expression:

                                                import Lean
                                                
                                                open Lean Meta
                                                
                                                def getFinBound (e : Expr) : MetaM (Option Expr) := do
                                                  let typewhnf (← inferType e)
                                                  let_expr Fin bound := type | return none
                                                  return bound
                                                
                                                def a : Fin 100 := 42
                                                
                                                run_meta
                                                  match ← getFinBound (.const ``a []) with
                                                  | some limit => IO.println (← ppExpr limit)
                                                  | none => IO.println "no limit found"
                                                
                                                Equations
                                                Instances For
                                                  @[always_inline]
                                                  Equations
                                                  Equations
                                                  Equations
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Equations
                                                  Equations
                                                  Instances For

                                                    Restore backtrackable parts of the state.

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

                                                      Incremental reuse primitive: if reusableResult? is none, runs act and returns its result together with the saved monadic state after act including the heartbeats used by it. If reusableResult? on the other hand is some (a, state), restores full state including heartbeats used and returns (a, state).

                                                      The intention is for steps that support incremental reuse to initially pass none as reusableResult? and store the result and state in a snapshot. In a further run, if reuse is possible, reusableResult? should be set to the previous result and state, ensuring that the state after running withRestoreOrSaveFull is identical in both runs. Note however that necessarily this is only an approximation in the case of heartbeats as heartbeats used by withRestoreOrSaveFull itself after calling act as well as by reuse-handling code such as the one supplying reusableResult? are not accounted for.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[inline]
                                                        def Lean.Meta.MetaM.run {α : Type} (x : Lean.MetaM α) (ctx : Lean.Meta.Context := { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all, univApprox := true, iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }, configKey := Lean.Meta.Config.toKey✝ { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all, univApprox := true, iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none, univApprox := false, inTypeClassResolution := false }) (s : Lean.Meta.State := { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, whnf := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, defEqTrans := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, defEqPerm := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } }, zetaDeltaFVarIds := , postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, diag := { unfoldCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, heuristicCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, instanceCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, synthPendingFailures := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } } }) :
                                                        Equations
                                                        • x.run ctx s = (x ctx).run s
                                                        Instances For
                                                          @[inline]
                                                          def Lean.Meta.MetaM.run' {α : Type} (x : Lean.MetaM α) (ctx : Lean.Meta.Context := { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all, univApprox := true, iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }, configKey := Lean.Meta.Config.toKey✝ { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all, univApprox := true, iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none, univApprox := false, inTypeClassResolution := false }) (s : Lean.Meta.State := { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, whnf := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, defEqTrans := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, defEqPerm := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } }, zetaDeltaFVarIds := , postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, diag := { unfoldCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, heuristicCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, instanceCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, synthPendingFailures := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } } }) :
                                                          Equations
                                                          • x.run' ctx s = Prod.fst <$> x.run ctx s
                                                          Instances For
                                                            @[inline]
                                                            def Lean.Meta.MetaM.toIO {α : Type} (x : Lean.MetaM α) (ctxCore : Lean.Core.Context) (sCore : Lean.Core.State) (ctx : Lean.Meta.Context := { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all, univApprox := true, iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }, configKey := Lean.Meta.Config.toKey✝ { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all, univApprox := true, iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none, univApprox := false, inTypeClassResolution := false }) (s : Lean.Meta.State := { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, whnf := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, defEqTrans := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, defEqPerm := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } }, zetaDeltaFVarIds := , postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, diag := { unfoldCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, heuristicCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, instanceCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, synthPendingFailures := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray } } }) :
                                                            Equations
                                                            • x.toIO ctxCore sCore ctx s = do let __discr(x.run ctx s).toIO ctxCore sCore match __discr with | ((a, s), sCore) => pure (a, sCore, s)
                                                            Instances For
                                                              @[inline]
                                                              def Lean.Meta.liftMetaM {m : TypeType u_1} {α : Type} [MonadLiftT Lean.MetaM m] (x : Lean.MetaM α) :
                                                              m α
                                                              Equations
                                                              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 α
                                                                Equations
                                                                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 α
                                                                  Equations
                                                                  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 α
                                                                    Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[inline]
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[inline]
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[inline]
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              Equations
                                                                              Instances For
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For

                                                                                          If diagnostics are enabled, record that declName has been unfolded.

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

                                                                                            If diagnostics are enabled, record that heuristic for solving f a =?= f b has been used.

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

                                                                                              If diagnostics are enabled, record that instance declName was used during TC resolution.

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

                                                                                                If diagnostics are enabled, record that synth pending failures.

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

                                                                                                            Return the array of postponed universe level constraints.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Set the array of postponed universe level constraints.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]

                                                                                                                Modify the array of postponed universe level constraints.

                                                                                                                Equations
                                                                                                                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.

                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  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 "head" of the top-level expression has been fully reduced. The result may contain subexpressions that have not been reduced.

                                                                                                                    See Lean.Meta.whnfImp for the implementation.

                                                                                                                    @[extern 6 lean_infer_type]

                                                                                                                    Returns the inferred type of the given expression. Assumes the expression is type-correct.

                                                                                                                    The type inference algorithm does not do general type checking. Type inference only looks at subterms that are necessary for determining an expression's type, and as such if inferType succeeds it does not mean the term is type-correct. If an expression is sufficiently ill-formed that it prevents inferType from computing a type, then it will fail with a type error.

                                                                                                                    For typechecking during elaboration, see Lean.Meta.check. (Note that we do not guarantee that the elaborator typechecker is as correct or as efficient as the kernel typechecker. The kernel typechecker is invoked when a definition is added to the environment.)

                                                                                                                    Here are examples of type-incorrect terms for which inferType succeeds:

                                                                                                                    import Lean
                                                                                                                    
                                                                                                                    open Lean Meta
                                                                                                                    
                                                                                                                    /--
                                                                                                                    `@id.{1} Bool Nat.zero`.
                                                                                                                    In general, the type of `@id α x` is `α`.
                                                                                                                    -/
                                                                                                                    def e1 : Expr := mkApp2 (.const ``id [1]) (.const ``Bool []) (.const ``Nat.zero [])
                                                                                                                    #eval inferType e1
                                                                                                                    -- Lean.Expr.const `Bool []
                                                                                                                    #eval check e1
                                                                                                                    -- error: application type mismatch
                                                                                                                    
                                                                                                                    /--
                                                                                                                    `let x : Int := Nat.zero; true`.
                                                                                                                    In general, the type of `let x := v; e`, if `e` does not reference `x`, is the type of `e`.
                                                                                                                    -/
                                                                                                                    def e2 : Expr := .letE `x (.const ``Int []) (.const ``Nat.zero []) (.const ``true []) false
                                                                                                                    #eval inferType e2
                                                                                                                    -- Lean.Expr.const `Bool []
                                                                                                                    #eval check e2
                                                                                                                    -- error: invalid let declaration
                                                                                                                    

                                                                                                                    Here is an example of a type-incorrect term that makes inferType fail:

                                                                                                                    /--
                                                                                                                    `Nat.zero Nat.zero`
                                                                                                                    -/
                                                                                                                    def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
                                                                                                                    #eval inferType e3
                                                                                                                    -- error: function expected
                                                                                                                    

                                                                                                                    See Lean.Meta.inferTypeImp for the implementation of inferType.

                                                                                                                    @[extern 7 lean_is_expr_def_eq]
                                                                                                                    @[extern 7 lean_is_level_def_eq]
                                                                                                                    @[extern 6 lean_synth_pending]
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      def Lean.Meta.withIncRecDepth {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                      n α
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              Instances For

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

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Return current transparency setting/mode.

                                                                                                                                  Equations
                                                                                                                                  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.

                                                                                                                                    Equations
                                                                                                                                    • mvarId.findDecl? = do let __do_liftLean.getMCtx pure (__do_lift.findDecl? mvarId)
                                                                                                                                    Instances For

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

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

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

                                                                                                                                        Equations
                                                                                                                                        • mvarId.getKind = do let __do_liftmvarId.getDecl pure __do_lift.kind
                                                                                                                                        Instances For

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

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

                                                                                                                                            Set mvarId kind in the current metavariable context.

                                                                                                                                            Equations
                                                                                                                                            Instances For

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

                                                                                                                                              Equations
                                                                                                                                              Instances For

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

                                                                                                                                                Equations
                                                                                                                                                • mvarId.isReadOnly = do let __do_liftmvarId.getDecl let __do_lift_1Lean.getMCtx pure (__do_lift.depth != __do_lift_1.depth)
                                                                                                                                                Instances For

                                                                                                                                                  Returns true if mvarId.isReadOnly returns true or if mvarId is a synthetic opaque metavariable.

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

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

                                                                                                                                                    Return the level of the given universe level metavariable.

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

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

                                                                                                                                                      Equations
                                                                                                                                                      • mvarId.isReadOnly = do let __do_liftmvarId.getLevel let __do_lift_1Lean.getMCtx pure (decide (__do_lift < __do_lift_1.levelAssignDepth))
                                                                                                                                                      Instances For

                                                                                                                                                        Set the user-facing name for the given metavariable.

                                                                                                                                                        Equations
                                                                                                                                                        Instances For

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

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

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

                                                                                                                                                            Equations
                                                                                                                                                            • fvarId.findDecl? = do let __do_liftLean.getLCtx pure (__do_lift.find? fvarId)
                                                                                                                                                            Instances For

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

                                                                                                                                                              Equations
                                                                                                                                                              • fvarId.getDecl = do let __do_liftLean.getLCtx match __do_lift.find? fvarId with | some d => pure d | none => liftM fvarId.throwUnknown
                                                                                                                                                              Instances For

                                                                                                                                                                Return the type of the given free variable.

                                                                                                                                                                Equations
                                                                                                                                                                • fvarId.getType = do let __do_liftfvarId.getDecl pure __do_lift.type
                                                                                                                                                                Instances For

                                                                                                                                                                  Return the binder information for the given free variable.

                                                                                                                                                                  Equations
                                                                                                                                                                  • fvarId.getBinderInfo = do let __do_liftfvarId.getDecl pure __do_lift.binderInfo
                                                                                                                                                                  Instances For

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

                                                                                                                                                                    Equations
                                                                                                                                                                    • fvarId.getValue? = do let __do_liftfvarId.getDecl pure __do_lift.value?
                                                                                                                                                                    Instances For

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

                                                                                                                                                                      Equations
                                                                                                                                                                      • fvarId.getUserName = do let __do_liftfvarId.getDecl pure __do_lift.userName
                                                                                                                                                                      Instances For

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

                                                                                                                                                                        Equations
                                                                                                                                                                        • fvarId.isLetVar = do let __do_liftfvarId.getDecl pure __do_lift.isLet
                                                                                                                                                                        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.

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For

                                                                                                                                                                            Returns true if another local declaration in the local context depends on fvarId.

                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            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.

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

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

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]

                                                                                                                                                                                  Lift a MkBindingM monadic action x to MetaM.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  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.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For

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

                                                                                                                                                                                      Equations
                                                                                                                                                                                      • e.abstractM xs = e.abstractRangeM xs.size xs
                                                                                                                                                                                      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.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          def Lean.Meta.mkForallFVars (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars : Lean.BinderInfo := Lean.BinderInfo.implicit) :

                                                                                                                                                                                          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.)
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Lean.Meta.mkLambdaFVars (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce : Bool := false) (binderInfoForMVars : Lean.BinderInfo := Lean.BinderInfo.implicit) :

                                                                                                                                                                                            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.

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

                                                                                                                                                                                                fun _ : Unit => a

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

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                      def Lean.Meta.withConfigWithKey {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (c : Lean.Meta.ConfigWithKey) :
                                                                                                                                                                                                      n αn α
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                          def Lean.Meta.withIncSynthPending {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} :
                                                                                                                                                                                                          n αn α
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                            def Lean.Meta.withInTypeClassResolution {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} :
                                                                                                                                                                                                            n αn α
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                              def Lean.Meta.withTrackingZetaDelta {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                                                              n α

                                                                                                                                                                                                              Executes x tracking zetaDelta reductions Config.trackZetaDelta := true

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                def Lean.Meta.withoutProofIrrelevance {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                                                                n α
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                  def Lean.Meta.withTransparency {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mode : Lean.Meta.TransparencyMode) :
                                                                                                                                                                                                                  n αn α
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                    def Lean.Meta.withDefault {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (x : n α) :
                                                                                                                                                                                                                    n α

                                                                                                                                                                                                                    withDefault x executes x using the default transparency setting.

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

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

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

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

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          @[inline]

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

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                          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.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                              def Lean.Meta.savingCache {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} :
                                                                                                                                                                                                                              n αn α
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  def Lean.Meta.withNewLocalInstance {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (className : Lean.Name) (fvar : Lean.Expr) :
                                                                                                                                                                                                                                  n αn α

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

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  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)
                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                    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 α
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      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 α) (cleanupAnnotations : Bool := false) :
                                                                                                                                                                                                                                        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.

                                                                                                                                                                                                                                        If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

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

                                                                                                                                                                                                                                          Given a monadic function f that takes a type and a term of that type and produces a new term, lifts this to the monadic function that opens a telescope, applies f to the body, and then builds the lambda telescope term for the new term.

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

                                                                                                                                                                                                                                            Given a monadic function f that takes a term and produces a new term, lifts this to the monadic function that opens a telescope, applies f to the body, and then builds the lambda telescope term for the new term.

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            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 α) (cleanupAnnotations : Bool := false) :
                                                                                                                                                                                                                                              n α

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

                                                                                                                                                                                                                                              If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                              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 α) (cleanupAnnotations : Bool := false) :
                                                                                                                                                                                                                                                n α

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

                                                                                                                                                                                                                                                If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                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 α) (cleanupAnnotations : Bool := false) :
                                                                                                                                                                                                                                                  n α

                                                                                                                                                                                                                                                  Similar to lambdaTelescope but for lambda and let expressions.

                                                                                                                                                                                                                                                  If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                  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 α) (cleanupAnnotations : Bool := false) :
                                                                                                                                                                                                                                                    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.

                                                                                                                                                                                                                                                    If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      def Lean.Meta.lambdaBoundedTelescope {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (e : Lean.Expr) (maxFVars : Nat) (k : Array Lean.ExprLean.Exprn α) (cleanupAnnotations : Bool := false) :
                                                                                                                                                                                                                                                      n α

                                                                                                                                                                                                                                                      Given e of the form fun ..xs ..ys => A, execute k xs (fun ..ys => A) where xs.size ≤ maxFVars. 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.

                                                                                                                                                                                                                                                      If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

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

                                                                                                                                                                                                                                                        Return the parameter names for the given global declaration.

                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                        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
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          Instances For

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

                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            Instances For

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

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                Similar to forallMetaTelescopeReducingAux but for lambda expressions.

                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  def Lean.Meta.withLocalDecl {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (name : Lean.Name) (bi : Lean.BinderInfo) (type : Lean.Expr) (k : Lean.Exprn α) (kind : Lean.LocalDeclKind := Lean.LocalDeclKind.default) :
                                                                                                                                                                                                                                                                  n α

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

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    def Lean.Meta.withLocalDeclD {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (name : Lean.Name) (type : Lean.Expr) (k : Lean.Exprn α) :
                                                                                                                                                                                                                                                                    n α
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                      Similar to withLocalDecl, but it does not check whether the new variable is a local instance or not.

                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        def Lean.Meta.withLocalDecls {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Lean.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.
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          partial def Lean.Meta.withLocalDecls.loop {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (declInfos : Array (Lean.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 (Lean.Name × (Array Lean.Exprn Lean.Expr))) (k : Array Lean.Exprn α) :
                                                                                                                                                                                                                                                                          n α
                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                          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.

                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              def Lean.Meta.withLetDecl {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (name : Lean.Name) (type val : Lean.Expr) (k : Lean.Exprn α) (kind : Lean.LocalDeclKind := Lean.LocalDeclKind.default) :
                                                                                                                                                                                                                                                                              n α

                                                                                                                                                                                                                                                                              Add the local declaration <name> : <type> := <val> 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.

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                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

                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  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.

                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                      Removes fvarId from the local context, and replaces occurrences of it with e. It is the responsibility of the caller to ensure that e is well-typed in the context of any occurrence of fvarId.

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        def Lean.Meta.withNewMCtxDepth {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (k : n α) (allowLevelAssignments : 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.)

                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        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.

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

                                                                                                                                                                                                                                                                                            Simpler version of withLCtx which just updates the local context. It is the resposability of the caller ensure the local instances are also properly updated.

                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              def Lean.Meta.withErasedFVars {n : TypeType} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} [Lean.MonadLCtx n] [MonadLiftT Lean.MetaM n] (fvarIds : Array Lean.FVarId) (k : n α) :
                                                                                                                                                                                                                                                                                              n α

                                                                                                                                                                                                                                                                                              Runs k in a local environment with the fvarIds erased.

                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                              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.

                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                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.

                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  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.

                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    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)]

                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      Instances For

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

                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                          whnf with at most instances transparency.

                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                          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.

                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                            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].

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              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

                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                  Pretty-print the given expression.

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

                                                                                                                                                                                                                                                                                                                    Pretty-print the given expression.

                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                      def Lean.Meta.orElse {α : Type} (x : Lean.MetaM α) (y : UnitLean.MetaM α) :
                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                        • Lean.Meta.instOrElseMetaM = { orElse := Lean.Meta.orElse }
                                                                                                                                                                                                                                                                                                                        @[inline]

                                                                                                                                                                                                                                                                                                                        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.

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

                                                                                                                                                                                                                                                                                                                          Execute x, and apply f to the produced error message

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                          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 α
                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                            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.

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

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

                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      def Lean.Meta.processPostponed (mayPostpone : Bool := true) (exceptionOnFailure : Bool := false) :
                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                        partial def Lean.Meta.processPostponed.loop (mayPostpone : Bool := true) (exceptionOnFailure : 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.

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

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

                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                            See isDefEq.

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

                                                                                                                                                                                                                                                                                                                                              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?

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

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

                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                    @[extern lean_checked_assign]

                                                                                                                                                                                                                                                                                                                                                    Returns true if mvarId := val was successfully assigned. This method uses the same assignment validation performed by isDefEq, but it does not check whether the types match.

                                                                                                                                                                                                                                                                                                                                                    Eta expand the given expression. Example:

                                                                                                                                                                                                                                                                                                                                                    etaExpand (mkConst ``Nat.add)
                                                                                                                                                                                                                                                                                                                                                    

                                                                                                                                                                                                                                                                                                                                                    produces fun x y => Nat.add x y

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

                                                                                                                                                                                                                                                                                                                                                      If e is of the form ?m ... instantiate metavars

                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                      Instances For