## Stream: general

### Topic: deleting variables

#### 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.)

no

#### Simon Hudon (Jun 03 2018 at 01:45):

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

#### 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


#### Reid Barton (Jun 03 2018 at 01:50):

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

#### Reid Barton (Jun 03 2018 at 01:50):

but I was hoping for something more convenient

#### 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

#### Simon Hudon (Jun 03 2018 at 01:50):

What is the inconvenient in doing that?

#### Reid Barton (Jun 03 2018 at 01:51):

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

#### 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

#### 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


#### Simon Hudon (Jun 03 2018 at 01:56):

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

#### 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

#### Simon Hudon (Jun 03 2018 at 02:01):

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

#### Mario Carneiro (Jun 03 2018 at 02:01):

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

Why?

#### 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

#### 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

#### 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

#### Mario Carneiro (Jun 03 2018 at 02:27):

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

#### 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