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
case _ : t => tacfinds the first goal that unifies with
tand then solves it using
tacor else fails. Like
show, it changes the type of the goal to
_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 => tacadditionally names the
mmost recent hypotheses with inaccessible names to the given names. The names are renamed before matching against
_can optionally be a case tag.
case _ : t := eis short for
case _ : t => exact e.
case _ : t₁ | _ : t₂ | ... => tacis 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 _ : twill 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 := ?mare the same as
case _ : tbut in the
?mcase the goal tag is changed to
m. In particular, the goal becomes metavariable
case' _ : t => tac is similar to the
case _ : t => tac tactic,
but it does not ensure the goal has been solved after applying
nor does it admit the goal if
case closes the goal using
and the tactic execution is not interrupted.
Find the first goal among those matching
tag whose type unifies with
renameI array consists of names to use to rename inaccessibles.
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.
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