Zulip Chat Archive

Stream: general

Topic: Inductive structures


view this post on Zulip James Kay (Jan 25 2021 at 19:36):

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?


Last updated: May 12 2021 at 22:15 UTC