Naming instance variables

Stream: new members

[Horatiu Cheval]

How can I give an explicit name for a class instance declared as a variable, so that I may refer to it later?
I.e. the following works, with the implicitly given name _inst_1:

@[class] inductive C : ℕ → Type
| mk : ∀ n, n > 0 → C n

variables (n : ℕ) [C n]

example : n > 0 :=
begin
  tactic.unfreeze_local_instances,
  cases _inst_1,
  assumption,
end

But if I try

variables (n : ℕ) [i : C n]

example : n > 0 :=
begin
  tactic.unfreeze_local_instances,
  cases i,
  assumption,
end

then i is not in scope, and neither is any implicit name.

[Shing Tak Lam]

does include i after the variables work?

[Reid Barton]

It's just that a named instance variable will not be included as a hypothesis automatically

[Reid Barton]

so anything which avoid relying on that (e.g. not using variables, not using tactic mode, using include) will avoid this problem

[Reid Barton]

If you have stuff like @[class] inductive that you need to case on, you should probably aim to minimize the number of times that you need to deal with that

[Horatiu Cheval]

The include solved it, thank you for the clarification