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 : Lake.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) (synthAssignedInstances : Bool) (allowSynthFailures : Bool) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.Meta.postprocessAppMVars (tacticName : Lake.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) (synthAssignedInstances : optParam Bool true) (allowSynthFailures : optParam 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
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.MVarId.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) :

            Close the given goal using apply e.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[irreducible]
              def Lean.MVarId.apply.go (mvarId : Lean.MVarId) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) (targetType : Lean.Expr) (eType : Lean.Expr) (rangeNumArgs : Std.Range) (i : Nat) :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[deprecated Lean.MVarId.apply]
                def Lean.Meta.apply (mvarId : Lean.MVarId) (e : Lean.Expr) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) :
                Equations
                Instances For
                  def Lean.MVarId.applyConst (mvar : Lean.MVarId) (c : Lake.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
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible, inline]

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

                      Equations
                      • mvarId.splitAnd = mvarId.splitAndCore
                      Instances For
                        @[deprecated Lean.MVarId.splitAnd]
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Lean.MVarId.nthConstructor (name : Lake.Name) (idx : Nat) (expected? : optParam (Option Nat) none) (goal : Lean.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
                            • One or more equations did not get rendered due to their size.
                            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
                              • One or more equations did not get rendered due to their size.
                              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
                                • One or more equations did not get rendered due to their size.
                                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
                                  • One or more equations did not get rendered due to their size.
                                  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
                                    • One or more equations did not get rendered due to their size.
                                    Instances For