No to_* on extended struct

Stream: new members

[Marcus Rossel]

In the following example, n.to_root does not work.

structure root (x : ℕ) := (a : ℕ)

structure next (x : ℕ) extends r : (root 0) := (b : r.a = 12)

example (n : next 1) : (root 0) := n.to_root

If I change this to the following, it works.

structure root (x : ℕ) := (a : ℕ)

structure next (x : ℕ) extends (root 0) := (b : to_root.a = 12)

example (n : next 1) : (root 0) := n.to_root

Why is that?

[Yakov Pechersky]

I'm not familiar with declaring a structure that extends a different one, and at the same time, providing a value for it

[Kyle Miller]

@Marcus Rossel The colon notation for extends is what names the function.

structure root (x : ℕ) := (a : ℕ)

structure next (x : ℕ) extends r : (root 0) := (b : r.a = 12)

example (n : next 1) : (root 0) := n.r

[Kyle Miller]

A helpful command to see what gets defined for the next structure is

#print prefix next