Zulip Chat Archive

Stream: general

Topic: Lean loves tactics


view this post on Zulip Patrick Massot (Jun 26 2018 at 18:45):

Why?

structure foo (X : Type) :=
(domain : set X)
(map : domain  X)


class bar (X : Type) :=
(foos : set (foo X))
(prop :  f  foos, by exact (set.range f.map = univ))

class bar' (X : Type) :=
(foos : set (foo X))
(prop :  f  foos, set.range f.map = univ) -- invalid field notation, type is not of the form (C ...) where C is a constant  f has type  ?m_1

view this post on Zulip Simon Hudon (Jun 26 2018 at 18:51):

I think that's because the type of f is not fully elaborated by the time f.map is parsed. If you wrote:

(prop :  f : foo _, f  foos -> set.range f.map = univ)

I think that should work

view this post on Zulip Patrick Massot (Jun 26 2018 at 18:54):

I guessed the issue comes from elaboration but couldn't see the fix

view this post on Zulip Patrick Massot (Jun 26 2018 at 18:54):

This fix indeed works

view this post on Zulip Patrick Massot (Jun 26 2018 at 18:55):

In the mean time I also realize that defining an auxiliary function from foo X to Prop also works

view this post on Zulip Patrick Massot (Jun 26 2018 at 18:55):

Thanks

view this post on Zulip Simon Hudon (Jun 26 2018 at 18:57):

Also has_mem has two type parameters so the type of is not enough to impose a type on f until type class resolution

view this post on Zulip Simon Hudon (Jun 26 2018 at 18:57):

:+1:

view this post on Zulip Patrick Massot (Jun 26 2018 at 18:58):

hum

view this post on Zulip Simon Hudon (Jun 26 2018 at 19:00):

Can I clarify something?

view this post on Zulip Patrick Massot (Jun 26 2018 at 19:00):

I think I sort of see

view this post on Zulip Chris Hughes (Jun 26 2018 at 19:04):

Does elaboration always happen before type class resolution?

view this post on Zulip Simon Hudon (Jun 26 2018 at 19:07):

I'm unsure whether elaboration is completed before type class resolution begins but most of it is done before type class resolution


Last updated: May 14 2021 at 14:20 UTC