## Stream: general

### Topic: Lean loves tactics

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


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

#### Patrick Massot (Jun 26 2018 at 18:54):

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

#### Patrick Massot (Jun 26 2018 at 18:54):

This fix indeed works

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

Thanks

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

:+1:

hum

#### Simon Hudon (Jun 26 2018 at 19:00):

Can I clarify something?

#### Patrick Massot (Jun 26 2018 at 19:00):

I think I sort of see

#### Chris Hughes (Jun 26 2018 at 19:04):

Does elaboration always happen before type class resolution?

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