Zulip Chat Archive

Stream: general

Topic: autoparam in instance

Patrick Massot (Dec 18 2018 at 11:48):

Is it possible to use autoparam in instances? I have a is_add_group_hom instance that never triggers, probably because is it contains a continuity assumption. The following doesn't seem to help:

instance sep_quot.is_add_group_hom_lift [separated β]  (hf : continuous f . tactic.assumption) : is_add_group_hom (sep_quot.lift f) := ...

Johan Commelin (Dec 18 2018 at 11:52):

Isn't this evidence that continuous should be a class?

Patrick Massot (Dec 18 2018 at 11:53):

Of course this also came to my mind

Patrick Massot (Dec 18 2018 at 11:53):

Here it would clearly help

Johan Commelin (Dec 18 2018 at 11:55):

/me doesn't know why group homs should be a class and continuous maps not...

Gabriel Ebner (Dec 18 2018 at 11:57):

Is it possible to use autoparam in instances?

No, auto_params are handled by the elaborator. Type class instance synthesis does not know about auto_param (or optional parameters).

Patrick Massot (Dec 18 2018 at 11:57):

Thanks Gabriel

Kenny Lau (Dec 18 2018 at 12:42):

neither should be a class

Kenny Lau (Dec 18 2018 at 12:42):

not group homs. not continuous maps. not linear maps.

Johan Commelin (Dec 18 2018 at 12:44):

So... what should be a class?

Kenny Lau (Dec 18 2018 at 12:50):

groups and topological spaces and modules?

Johan Commelin (Dec 18 2018 at 12:51):

Why???

Kenny Lau (Dec 18 2018 at 12:52):

how is it done in your category theory?

Kevin Buzzard (Dec 18 2018 at 13:17):

Continuous maps not a class -- Johannes has explained this before on this forum, although I have never really internalised the issue.

Last updated: Dec 20 2023 at 11:08 UTC