Documentation

Batteries.Tactic.Case

Extensions to the case tactic #

Adds a variant of case that looks for a goal with a particular type, rather than a goal with a particular tag. For consistency with case, it takes a tag as well, but the tag can be a hole _.

Also adds case' extensions.

source
def Batteries.Tactic.casePattArg :
Lean.ParserDescr

Clause for a case ... : ... tactic.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Batteries.Tactic.casePattTac :
    Lean.ParserDescr

    The body of a case ... | ... tactic that's a tactic sequence (or hole).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Batteries.Tactic.casePattExpr :
      Lean.ParserDescr

      The body of a case ... | ... tactic that's an exact term.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Batteries.Tactic.casePattBody :
        Lean.ParserDescr

        The body of a case ... : ... tactic.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Batteries.Tactic.casePatt :
          Lean.ParserDescr
          • case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.
          • case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.
          • case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).

          Extensions:

          • case _ : t => tac finds the first goal that unifies with t and then solves it using tac or else fails. Like show, it changes the type of the goal to t. The _ can optionally be a case tag, in which case it only looks at goals whose tag would be considered by case (goals with an exact tag match, followed by goals with the tag as a suffix, followed by goals with the tag as a prefix).

          • case _ n₁ ... nₘ : t => tac additionally names the m most recent hypotheses with inaccessible names to the given names. The names are renamed before matching against t. The _ can optionally be a case tag.

          • case _ : t := e is short for case _ : t => exact e.

          • case _ : t₁ | _ : t₂ | ... => tac is equivalent to (case _ : t₁ => tac); (case _ : t₂ => tac); ... but with all matching done on the original list of goals -- each goal is consumed as they are matched, so patterns may repeat or overlap.

          • case _ : t will make the matched goal be the first goal. case _ : t₁ | _ : t₂ | ... makes the matched goals be the first goals in the given order.

          • case _ : t := _ and case _ : t := ?m are the same as case _ : t but in the ?m case the goal tag is changed to m. In particular, the goal becomes metavariable ?m.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Batteries.Tactic.casePatt' :
            Lean.ParserDescr

            case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

            Extensions:

            • case' _ : t => tac is analogous to the case _ : t => tac variant.
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Batteries.Tactic.findGoalOfPatt (gs : List Lean.MVarId) (tag : Lean.TSyntax `Lean.binderIdent) (patt? : Option Lean.Term) (renameI : Lean.TSyntaxArray `Lean.binderIdent) :
              Lean.Elab.Tactic.TacticM (Lean.MVarId × List Lean.MVarId × List Lean.MVarId)

              Find the first goal among those matching tag whose type unifies with patt. The renameI array consists of names to use to rename inaccessibles. The patt term is elaborated in the context where the inaccessibles have been renamed.

              Returns the found goal, goals caused by elaborating patt, and the remaining goals.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Batteries.Tactic.processCasePattBody (stx : Lean.TSyntax `Batteries.Tactic.casePattTac) :
                Lean.Elab.Tactic.TacticM (Lean.Term ⊕ Lean.Syntax × Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

                Given a casePattBody, either give a synthetic hole or a tactic sequence (along with the syntax for the =>). Converts holes into synthetic holes since they are processed with elabTermWithHoles.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Batteries.Tactic.evalCase (close : Bool) (stx : Lean.Syntax) (tags : Array (Lean.TSyntax `Lean.binderIdent)) (hss : Array (Lean.TSyntaxArray `Lean.binderIdent)) (patts? : Array (Option Lean.Term)) (caseBody : Lean.TSyntax `Batteries.Tactic.casePattTac) :
                  Lean.Elab.Tactic.TacticM Unit

                  Implementation for case and case'.

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