deleting variables

Stream: general

[Reid Barton]

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

[Kenny Lau]

no

[Simon Hudon]

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

[Reid Barton]

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]

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

[Reid Barton]

but I was hoping for something more convenient

[Simon Hudon]

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

[Simon Hudon]

What is the inconvenient in doing that?

[Reid Barton]

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

[Simon Hudon]

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]

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]

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

[Reid Barton]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Simon Hudon]

Why?

[Mario Carneiro]

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]

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]

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]

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

[Simon Hudon]

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