Mutual recursion between inductive types and structures

Stream: new members

[Will Crichton]

The Lean book claims that structures are essentially syntax sugar for inductive types, like these two definitions of prod:

inductive Prod (α : Type u) (β : Type v) where
  | mk (fst : α) (snd : β) : Prod α β

structure Prod (α : Type u) (β : Type v) where
  mk :: (fst : α) (snd : β)

The Lean book says:

In Lean, the keyword structure can be used to define such an inductive type as well as its projections, at the same time.

However, I really want to make a structure mutually recursive with an inductive type:

mutual
  inductive ElementKind
    | text (s : String)
    | group (g : List Element)

  structure Element where
    kind : ElementKind
    box : Box
end

But Lean rejects this, saying I have to define Element as an inductive type. Is there a workaround that lets me define Element as a structure? Or is it fundamentally important that Element be defined via inductive?

[Chris Bailey]

Only a subset of inductive types can be structures. They can only have one constructor, cannot be recursive, and cannot have indices.

[Will Crichton]

That makes sense. Perhaps a different question is: is there a way to get the ergonomics of structures with structure-like inductive types? Eg I really enjoy the curly-brace syntax with field punning and such.

[Will Crichton]

^ bumping this again in case anyone has an answer. It's quite frustrating to not be able to define complex tree types using auxiliary structure definitions. Is the only solution to define more single-branch inductive types?

[Kyle Miller]

Sorry to say it's not supported yet, but I hope to see it in the not-too-distant future

[Will Crichton]

Got it, I'll keep my eyes on the changelogs!