dot notation transitive discovery

Stream: general

[Eric Wieser]

How on earth does this work?

import algebra.module.basic

def wat {R M : Type*} [semiring R] [add_comm_monoid M] (h : semimodule R M) : has_scalar R M :=
h.to_has_scalar

#print semimodule.to_has_scalar -- doesn't exist

set_option pp.implicit true
#print wat -- a long chain of projections!

[Eric Wieser]

Oh, it's only available on new structures:

import algebra.module.basic

namespace new

structure A1 := (x : ℕ)
structure A2 extends A1.
structure A3 extends A2.

example (a : A3) : A1 := a.to_A1  -- ok

end new

namespace old

set_option old_structure_cmd true

structure A1 := (x : ℕ)
structure A2 extends A1.
structure A3 extends A2.

example (a : A3) : A1 := a.to_A1  -- fail

end old

[Eric Wieser]

Do we have documentation for it? docs#old_structure_cmd?

[Oliver Nash]

I would have guessed this was the other way round. I note that:

example (a : A3) : A1 := a.to_A2.to_A1

works.