Documentation

Lean.Elab.Tactic.ElabTerm

elabTerm for Tactics and basic tactics that use it. #

Runs a term elaborator inside a tactic.

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    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
    • One or more equations did not get rendered due to their size.
    Instances For

      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
      • One or more equations did not get rendered due to their size.
      Instances For

        Try to close main goal using x target, where target is the type of the main goal.

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

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

                  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

                      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 main goal's tag. If multiple unnamed goals are encountered, tagSuffix is appended to the main goal's 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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Lean.Elab.Tactic.refineCore (stx : Lean.Syntax) (tagSuffix : Lake.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 ?.

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

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

                                          Elaborate stx. If it 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
                                          • 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
                                              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