induction variables

Stream: general

[Thorsten Altenkirch]

What is the recommended way to supply variable name to induction and cases? I have been using with but this becomes unwieldy for more complicated inductive types.

[Mario Carneiro]

You can also use case, which reads better especially for big inductive types

[Mario Carneiro]

inductive foo
| a : ℕ → foo
| b : ℕ → ℕ → foo
| c : foo → ℕ → foo

example : foo → false :=
begin
  intro x,
  induction x,
  case a : n {
    sorry, },
  case b : m n {
    sorry, },
  case c : x n IH {
    sorry, },
end