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.

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

Instances For

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

    Instances For

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

      Instances For

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

        Instances For
          • 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.

          Instances For

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

            Instances For

              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.

              Instances For
                def Std.Tactic.processCasePattBody (stx : Lean.TSyntax `Std.Tactic.casePattTac) :

                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.

                Instances For
                  def Std.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 `Std.Tactic.casePattTac) :

                  Implementation for case and case'.

                  Instances For