Zulip Chat Archive

Stream: general

Topic: deleting variables


view this post on Zulip Reid Barton (Jun 03 2018 at 01:44):

Is it possible to delete something that has been declared using variables? (I want to "upgrade" an instance variable to a class which extends the original one.)

view this post on Zulip Kenny Lau (Jun 03 2018 at 01:44):

no

view this post on Zulip Simon Hudon (Jun 03 2018 at 01:45):

Can you show me concretely what you're going for?

view this post on Zulip Reid Barton (Jun 03 2018 at 01:49):

My actual example involves my own classes, but something like

section
variables {α : Type} [monoid α]

/- other definitions that don't require the group structure... -/

variables [group α]

def g : α  α := λ x, x * x⁻¹
example (x : α) : g x = (1 : α) := by simp [g]

end

view this post on Zulip Reid Barton (Jun 03 2018 at 01:50):

I can just put the earlier definitions in their own section which has the monoid variable

view this post on Zulip Reid Barton (Jun 03 2018 at 01:50):

but I was hoping for something more convenient

view this post on Zulip Simon Hudon (Jun 03 2018 at 01:50):

Ah I see! Your best bet I think is to end your section and start it just before the group variable

view this post on Zulip Simon Hudon (Jun 03 2018 at 01:50):

What is the inconvenient in doing that?

view this post on Zulip Reid Barton (Jun 03 2018 at 01:51):

Not really very inconvenient, just a few extra lines of section/end

view this post on Zulip Simon Hudon (Jun 03 2018 at 01:53):

One downside I can see is if you have other variables declared in the first section that you want to keep in the rest of the section

view this post on Zulip Simon Hudon (Jun 03 2018 at 01:54):

In that case, I would do this:

section
variables {α : Type}
section
variables [monoid α]

/- other definitions that don't require the group structure... -/
end
variables [group α]
end

view this post on Zulip Simon Hudon (Jun 03 2018 at 01:56):

Actually, if you don't do anything, what error do you get?

view this post on Zulip Reid Barton (Jun 03 2018 at 02:00):

There I got an error which arose because * was using the monoid instance and \-1 was using the group instance

view this post on Zulip Simon Hudon (Jun 03 2018 at 02:01):

Ah, ok, I thought maybe it would go through the group by default

view this post on Zulip Mario Carneiro (Jun 03 2018 at 02:01):

well it's still a problem to have redundant typeclasses on a def

view this post on Zulip Simon Hudon (Jun 03 2018 at 02:04):

Why?

view this post on Zulip Mario Carneiro (Jun 03 2018 at 02:05):

in the theorem itself, it's a problem since they aren't the same structure, in uses it's a nuisance to have a redundant assumption

view this post on Zulip Simon Hudon (Jun 03 2018 at 02:07):

Right in theorems I know the issues. With defs, I can't see it will be a nuisance down the line but not how that definition would be invalid

view this post on Zulip Mario Carneiro (Jun 03 2018 at 02:27):

It won't be invalid. Often things like duplicate typeclass hypotheses will go unnoticed for a long time because they aren't really visibly different

view this post on Zulip Mario Carneiro (Jun 03 2018 at 02:27):

unless you use @thm and notice two underscores in place of one

view this post on Zulip Simon Hudon (Jun 03 2018 at 02:30):

It would be nice to have warnings for that kind of stuff. Actually, more warnings in general would be nice


Last updated: May 10 2021 at 00:31 UTC