Lean loves tactics

Stream: general

[Patrick Massot]

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]

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]

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

[Patrick Massot]

This fix indeed works

[Patrick Massot]

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

[Patrick Massot]

Thanks

[Simon Hudon]

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

[Simon Hudon]

:+1:

[Patrick Massot]

hum

[Simon Hudon]

Can I clarify something?

[Patrick Massot]

I think I sort of see

[Chris Hughes]

Does elaboration always happen before type class resolution?

[Simon Hudon]

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