Documentation

Lean.Meta.Tactic.Apply

Compute the number of expected arguments and whether the result type is of the form (?m ...) where ?m is an unassigned metavariable.

Equations
    Instances For
      Equations
        Instances For
          def Lean.Meta.synthAppInstances (tacticName : Name) (mvarId : MVarId) (mvarsNew : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances allowSynthFailures : Bool) :
          Equations
            Instances For
              def Lean.Meta.synthAppInstances.step (tacticName : Name) (mvarId : MVarId) (allowSynthFailures : Bool) (mvars : Array Expr) :

              Try to synthesize instances for the metavariables mvars. Returns metavariables that still need to be synthesized. We can view the resulting array as the set of metavariables that we should try again. This is needed when applying or rewriting with functions with complex instances. For example, consider rw [@map_smul] where map_smul is

              map_smul {F : Type u_1} {M : Type u_2} {N : Type u_3} {φ : M → N}
                       {X : Type u_4} {Y : Type u_5}
                       [SMul M X] [SMul N Y] [FunLike F X Y] [MulActionSemiHomClass F φ X Y]
                       (f : F) (c : M) (x : X) : DFunLike.coe f (c • x) = φ c • DFunLike.coe f x
              

              and MulActionSemiHomClass is defined as

              class MulActionSemiHomClass (F : Type _)
                 {M N : outParam (Type _)} (φ : outParam (M → N))
                 (X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
              

              The left-hand-side of the equation does not bind N. Thus, SMul N Y cannot be synthesized until we synthesize MulActionSemiHomClass F φ X Y. Note that N is an output parameter for MulActionSemiHomClass.

              Equations
                Instances For
                  def Lean.Meta.appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) :
                  Equations
                    Instances For
                      def Lean.Meta.postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances : Bool := true) (allowSynthFailures : Bool := false) :

                      If synthAssignedInstances is true, then apply will synthesize instance implicit arguments even if they have assigned by isDefEq, and then check whether the synthesized value matches the one inferred. The congr tactic sets this flag to false.

                      Equations
                        Instances For
                          def Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : Meta.ApplyConfig := { }) (term? : Option MessageData := none) :

                          Close the given goal using apply e.

                          Equations
                            Instances For
                              @[irreducible]
                              def Lean.MVarId.apply.go (mvarId : MVarId) (cfg : Meta.ApplyConfig := { }) (term? : Option MessageData := none) (targetType eType : Expr) (rangeNumArgs : Std.Range) (i : Nat) :
                              Equations
                                Instances For

                                  Short-hand for applying a constant to the goal.

                                  Equations
                                    Instances For
                                      def Lean.MVarId.applyN (mvarId : MVarId) (e : Expr) (n : Nat) (useApproxDefEq : Bool := true) :

                                      Close the given goal using e, instantiated with n metavariables.

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

                                              Apply And.intro as much as possible to goal mvarId.

                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      def Lean.MVarId.nthConstructor (name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :

                                                      Apply the n-th constructor of the target type, checking that it is an inductive type, and that there are the expected number of constructors.

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

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

                                                              Equations
                                                                Instances For

                                                                  Try to close the goal 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.

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

                                                                      Equations
                                                                        Instances For