Documentation

Lean.Elab.Tactic.ElabTerm

elabTerm for Tactics and basic tactics that use it. #

def Lean.Elab.Tactic.runTermElab {α : Type} (k : TermElabM α) (mayPostpone : Bool := false) :

Runs a term elaborator inside a tactic.

This function ensures that term elaboration fails when backtracking, i.e., in first| tac term | other.

Equations
    Instances For
      def Lean.Elab.Tactic.runTermElab.go {α : Type} (k : TermElabM α) (mayPostpone : Bool := false) :
      Equations
        Instances For
          def Lean.Elab.Tactic.elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone : Bool := false) :

          Elaborate stx in the current MVarContext. If given, the expectedType will be used to help elaboration but not enforced (use elabTermEnsuringType to enforce an expected type).

          Equations
            Instances For
              def Lean.Elab.Tactic.elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone : Bool := false) :

              Elaborate stx in the current MVarContext. If given, the expectedType will be used to help elaboration and then a TypeMismatchError will be thrown if the elaborated type doesn't match.

              Equations
                Instances For
                  def Lean.Elab.Tactic.filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) :
                  Equations
                    Instances For
                      def Lean.Elab.Tactic.closeMainGoalUsing (tacName : Name) (x : ExprNameTacticM Expr) (checkNewUnassigned : Bool := true) :

                      Try to close main goal using x target tag, where target is the type of the main goal and tag is its user name.

                      If checkNewUnassigned is true, then throws an error if the resulting value has metavariables that were created during the execution of x. If it is false, then it is the responsibility of x to add such metavariables to the goal list.

                      During the execution of x:

                      • The local context is that of the main goal.
                      • The goal list has the main goal removed.
                      • It is allowable to modify the goal list, for example with Lean.Elab.Tactic.pushGoals.

                      On failure, the main goal remains at the front of the goal list.

                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      def Lean.Elab.Tactic.withCollectingNewGoalsFrom (k : TacticM Expr) (parentTag tagSuffix : Name) (allowNaturalHoles : Bool := false) :

                                      Execute k, and collect new "holes" in the resulting expression.

                                      • parentTag and tagSuffix are used to tag untagged goals with Lean.Elab.Tactic.tagUntaggedGoals.
                                      • If allowNaturalHoles is true, then _'s are allowed and create new goals.
                                      Equations
                                        Instances For
                                          def Lean.Elab.Tactic.withCollectingNewGoalsFrom.go (k : TacticM Expr) (parentTag tagSuffix : Name) (allowNaturalHoles : Bool := false) :
                                          Equations
                                            Instances For
                                              def Lean.Elab.Tactic.elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles : Bool := false) (parentTag? : Option Name := none) :

                                              Elaborates stx and collects the MVarIds of any holes that were created during elaboration.

                                              With allowNaturalHoles := false (the default), any new natural holes (_) which cannot be synthesized during elaboration cause elabTermWithHoles to fail. (Natural goals appearing in stx which were created prior to elaboration are permitted.)

                                              Unnamed MVarIds are renamed to share the tag parentTag? (or the main goal's tag if parentTag? is none). If multiple unnamed goals are encountered, tagSuffix is appended to this tag along with a numerical index.

                                              Note:

                                              • Previously-created MVarIds which appear in stx are not returned.
                                              • All parts of elabTermWithHoles operate at the current MCtxDepth, and therefore may assign metavariables.
                                              • When allowNaturalHoles := true, stx is elaborated under withAssignableSyntheticOpaque, meaning that .syntheticOpaque metavariables might be assigned during elaboration. This is a consequence of the implementation.
                                              Equations
                                                Instances For
                                                  def Lean.Elab.Tactic.refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) :

                                                  If allowNaturalHoles == true, then we allow the resultant expression to contain unassigned "natural" metavariables. Recall that "natutal" metavariables are created for explicit holes _ and implicit arguments. They are meant to be filled by typing constraints. "Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation ?<hole-name>.

                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For

                                                              Given a tactic

                                                              apply f
                                                              

                                                              we want the apply tactic to create all metavariables. The following definition will return @f for f. That is, it will not create metavariables for implicit arguments. A similar method is also used in Lean 3. This method is useful when applying lemmas such as:

                                                              theorem infLeRight {s t : Set α} : s ⊓ t ≤ t
                                                              

                                                              where s ≤ t here is defined as

                                                              ∀ {x : α}, x ∈ s → x ∈ t
                                                              
                                                              Equations
                                                                Instances For
                                                                  Equations
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          Equations
                                                                            Instances For
                                                                              Equations
                                                                                Instances For

                                                                                  Elaborate stx. If it is a free variable, return it. Otherwise, assert it, and return the free variable. Note that, the main goal is updated when Meta.assert is used in the second case.

                                                                                  Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              def Lean.Elab.Tactic.evalDecideCore.doElab (tacticName : Name) (expectedType : Expr) :
                                                                                              Equations
                                                                                                Instances For
                                                                                                  def Lean.Elab.Tactic.evalDecideCore.doKernel (tacticName : Name) (expectedType : Expr) :
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      def Lean.Elab.Tactic.evalDecideCore.diagnose (tacticName : Name) {α : Type} (expectedType s : Expr) (r? : Option Expr) :
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                            Instances For