match
performs case analysis on one or more expressions.
See Induction and Recursion.
The syntax for the match
tactic is the same as term-mode match
, except that
the match arms are tactics instead of expressions.
example (n : Nat) : n = n := by
match n with
| 0 => rfl
| i+1 => simp
Equations
Instances For
The tactic
intro
| pat1 => tac1
| pat2 => tac2
is the same as:
intro x
match x with
| pat1 => tac1
| pat2 => tac2
That is, intro
can be followed by match arms and it introduces the values while
doing a pattern match. This is equivalent to fun
with match arms in term mode.