Documentation

Std.Lean.Meta.Basic

Sort the given FVarIds by the order in which they appear in the current local context. If any of the FVarIds do not appear in the current local context, the result is unspecified.

Equations
Instances For

    Get the MetavarDecl of mvarId. If mvarId is not a declared metavariable in the given MetavarContext, throw an error.

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

      Declare a metavariable. You must make sure that the metavariable is not already declared.

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

        Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.

        Equations
        Instances For

          Check whether a metavariable is declared in the given MetavarContext.

          Equations
          Instances For

            Erase any assignment or delayed assignment of the given metavariable.

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

              Modify the declaration of a metavariable. If the metavariable is not declared, the MetavarContext is returned unchanged.

              You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

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

                Modify the local context of a metavariable. If the metavariable is not declared, the MetavarContext is returned unchanged.

                You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

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

                  Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, the MetavarContext is returned unchanged.

                  Equations
                  Instances For

                    Set the BinderInfo of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, the MetavarContext is returned unchanged.

                    Equations
                    Instances For

                      Obtain all unassigned metavariables from the given MetavarContext. If includeDelayed is true, delayed-assigned metavariables are considered unassigned.

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

                        Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.

                        Equations
                        Instances For

                          Check whether a metavariable is declared.

                          Equations
                          Instances For

                            Erase any assignment or delayed assignment of the given metavariable.

                            Equations
                            Instances For

                              Modify the declaration of a metavariable. If the metavariable is not declared, nothing happens.

                              You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

                              Equations
                              Instances For

                                Modify the local context of a metavariable. If the metavariable is not declared, nothing happens.

                                You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

                                Equations
                                Instances For

                                  Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.

                                  Equations
                                  Instances For

                                    Set the BinderInfo of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.

                                    Equations
                                    Instances For

                                      Collect the metavariables which mvarId depends on. These are the metavariables which appear in the type and local context of mvarId, as well as the metavariables which those metavariables depend on, etc.

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

                                        Check if a goal is of a subsingleton type.

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

                                          Check if a goal is "independent" of a list of other goals. We say a goal is independent of other goals if assigning a value to it can not change the assignability of the other goals.

                                          Examples:

                                          • ?m_1 : Type is not independent of ?m_2 : ?m_1, because we could assign true : Bool to ?m_2, but if we first assign Nat to ?m_1 then that is no longer possible.
                                          • ?m_1 : Nat is not independent of ?m_2 : Fin ?m_1, because we could assign 37 : Fin 42 to ?m_2, but if we first assign 2 to ?m_1 then that is no longer possible.
                                          • ?m_1 : ?m_2 is not independent of ?m_2 : Type, because we could assign Bool to ?m_2, but if we first assign 0 : Natto?m_1` then that is no longer possible.
                                          • Given P : Prop and f : P → Type, ?m_1 : P is independent of ?m_2 : f ?m_1 by proof irrelevance.
                                          • Similarly given f : Fin 0 → Type, ?m_1 : Fin 0 is independent of ?m_2 : f ?m_1, because Fin 0 is a subsingleton.
                                          • Finally ?m_1 : Nat is independent of ?m_2 : α, as long as ?m_1 does not appear in Meta.getMVars α (note that Meta.getMVars follows delayed assignments).

                                          This function only calculates a conservative approximation of this condition. That is, it may return false when it should return true. (In particular it returns false whenever the type of g contains a metavariable, regardless of whether this is related to the metavariables in L.)

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

                                            Solve a goal by synthesizing an instance.

                                            Equations
                                            Instances For

                                              Replace hypothesis hyp in goal g with proof : typeNew. The new hypothesis is given the same user name as the original, it attempts to avoid reordering hypotheses, and the original is cleared if possible.

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

                                                Finds the LocalDecl for the FVar in e with the highest index.

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

                                                  Add the hypothesis h : t, given v : t, and return the new FVarId.

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

                                                    Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

                                                    Equations
                                                    Instances For
                                                      def Lean.MVarId.applyConst (mvar : Lean.MVarId) (c : Lean.Name) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) :

                                                      Short-hand for applying a constant to the goal.

                                                      Equations
                                                      Instances For

                                                        Obtain all unassigned metavariables. If includeDelayed is true, delayed-assigned metavariables are considered unassigned.

                                                        Equations
                                                        Instances For
                                                          def Lean.Meta.unhygienic {m : TypeType} {α : Type} [Lean.MonadWithOptions m] (x : m α) :
                                                          m α

                                                          Run a computation with hygiene turned off.

                                                          Equations
                                                          Instances For

                                                            A variant of mkFreshId which generates names with a particular prefix. The generated names are unique and have the form <prefix>.<N> where N is a natural number. They are not suitable as user-facing names.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Lean.Meta.repeat'Core {m : TypeType} {ε : Type u_1} {s : Type} [Monad m] [MonadExcept ε m] [Lean.MonadBacktrack s m] [Lean.MonadMCtx m] (f : Lean.MVarIdm (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) :

                                                              Implementation of repeat' and repeat1'.

                                                              repeat'Core f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred.

                                                              Returns a boolean indicating whether f succeeded at least once, and all the remaining goals (i.e. those on which f failed).

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

                                                                Auxiliary for repeat'Core. repeat'Core.go f maxIters progress gs stk acc evaluates to essentially acc.toList ++ repeat' f (gs::stk).join maxIters: that is, acc are goals we will not revisit, and (gs::stk).join is the accumulated todo list of subgoals.

                                                                Equations
                                                                Instances For
                                                                  def Lean.Meta.repeat' {m : TypeType} {ε : Type u_1} {s : Type} [Monad m] [MonadExcept ε m] [Lean.MonadBacktrack s m] [Lean.MonadMCtx m] (f : Lean.MVarIdm (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) :

                                                                  repeat' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Always succeeds (returning the original goals if f fails on all of them).

                                                                  Equations
                                                                  Instances For
                                                                    def Lean.Meta.repeat1' {m : TypeType} {ε : Type u_1} {s : Type} [Monad m] [Lean.MonadError m] [MonadExcept ε m] [Lean.MonadBacktrack s m] [Lean.MonadMCtx m] (f : Lean.MVarIdm (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) :

                                                                    repeat1' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Fails if f does not succeed at least once.

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

                                                                      saturate1 goal tac runs tac on goal, then on the resulting goals, etc., until tac does not apply to any goal any more (i.e. it returns none). The order of applications is depth-first, so if tac generates goals [g₁, g₂, ⋯], we apply tac to g₁ and recursively to all its subgoals before visiting g₂. If tac does not apply to goal, saturate1 returns none. Otherwise it returns the generated subgoals to which tac did not apply. saturate1 respects the MonadRecDepth recursion limit.

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

                                                                        Auxiliary definition for saturate1.

                                                                        Return local hypotheses which are not "implementation detail", as Exprs.

                                                                        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