Documentation

Lean.Meta.Tactic.Apply

Controls which new mvars are turned in to goals by the apply tactic.

  • nonDependentFirst mvars that don't depend on other goals appear first in the goal list.
  • nonDependentOnly only mvars that don't depend on other goals are added to goal list.
  • all all unassigned mvars are added to the goal list.
Instances For
    • synthAssignedInstances : Bool

      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.

    • allowSynthFailures : Bool

      If allowSynthFailures is true, then apply will return instance implicit arguments for which typeclass search failed as new goals.

    • approx : Bool

      If approx := true, then we turn on isDefEq approximations. That is, we use the approxDefEq combinator.

    Configures the behaviour of the apply tactic.

    Instances For

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

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

                        Equations
                        Instances For
                          @[deprecated Lean.MVarId.splitAnd]
                          Equations
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For