Zulip Chat Archive

Stream: new members

Topic: Naming instance variables


view this post on Zulip Horatiu Cheval (Jan 14 2021 at 17:48):

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.

view this post on Zulip Shing Tak Lam (Jan 14 2021 at 17:49):

does include i after the variables work?

view this post on Zulip Reid Barton (Jan 14 2021 at 17:49):

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

view this post on Zulip Reid Barton (Jan 14 2021 at 17:50):

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

view this post on Zulip Reid Barton (Jan 14 2021 at 17:51):

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

view this post on Zulip Horatiu Cheval (Jan 14 2021 at 17:58):

The include solved it, thank you for the clarification


Last updated: May 14 2021 at 21:11 UTC