Inductive structures

Stream: general

[James Kay]

Is it impossible to refer inductively to the type being defined when using structure?

inductive Wind (α : Type 0) (f : α → Type 0) : Type 1
| sup (head : α) (tail : f head → Wind) : Wind

This type works fine, but if I try to convert it to a structure so I can use e.g. field projections,

structure Wstr (α : Type 0) (f : α → Type 0) :=
(head : α)
(tail : f head → Wstr α f)

I get an error about Wstr not being in scope. Do I just have to use inductive even though it has only one constructor, and write all my projections and so forth manually? Or is there some additional syntax I'm missing? The manual says that structure is just sugar on top of inductive, so I expected to be able to do this. Or can I perhaps define an inductive type such that Lean recognizes it as a structure and lets me use record syntax and things?