Documentation

Mathlib.Lean.Meta

Additional utilities in Lean.MVarId #

Solve a goal by synthesizing an instance.

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.

    Instances For

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

      Instances For

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

        Instances For

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

          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.

            Instances For

              Has the effect of refine ⟨e₁,e₂,⋯, ?_⟩.

              Instances For

                Applies intro repeatedly until it fails. We use this instead of Lean.MVarId.intros to allowing unfolding. For example, if we want to do introductions for propositions like ¬p, the ¬ needs to be unfolded into False, and intros does not do such unfolding.

                Instances For

                  Check if a goal is of a subsingleton type.

                  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 solvability of the other goals.

                    This function only calculates a conservative approximation of this condition.

                    Instances For

                      Try to convert an Iff into an Eq by applying iff_of_eq. If successful, returns the new goal, and otherwise returns the original MVarId.

                      This may be regarded as being a special case of Lean.MVarId.liftReflToEq, specifically for Iff.

                      Instances For

                        Try to convert an Eq into an Iff by applying propext. If successful, then returns then new goal, otherwise returns the original MVarId.

                        Instances For

                          Try to close the goal with using proof_irrel_heq. Returns whether or not it succeeds.

                          We need to be somewhat careful not to assign metavariables while doing this, otherwise we might specialize Sort _ to Prop.

                          Instances For

                            Try to close the goal using Subsingleton.elim. Returns whether or not it succeeds.

                            We are careful to apply Subsingleton.elim in a way that does not assign any metavariables. This is to prevent the Subsingleton Prop instance from being used as justification to specialize Sort _ to Prop.

                            Instances For

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

                              Instances For

                                Count how many local hypotheses appear in an expression.

                                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.

                                  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.

                                    Instances For

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

                                      Instances For

                                        Analogue of liftMetaTactic for tactics that return a single goal.

                                        Instances For

                                          Analogue of liftMetaTactic for tactics that do not return any goals.

                                          Instances For

                                            Copy of Lean.Elab.Tactic.run that can return a value.

                                            Instances For