mutually defined inductive type and structure

Stream: general

[Bhakti Shah]

Is there a way to write something like

mutual
    inductive t1 where
    | C1
    | C2 (a : t2)

    structure t2 where
    k : t1
    v : Nat
end

where you have a structure and an inductive type mutually defined? I think currently you can only use a mutual block for multiple defs or inductive types

[Max Nowak 🐉]

Structures are just inductive types with one constructor and which are not recursive. So there is no point in putting them in a mutual block, as the only time you need a mutual block is when both types are recursive, I think?

[Bhakti Shah]

yeah, I agree -- however there's no other way to use t2 in the definition of t1 and vice versa without defining them in a mutual block as far as I'm aware, and I'm not sure what the syntax for the same would be if not mutual

[Bhakti Shah]

I guess when I said mutually defined i didn't necessarily mean mutual induction or recursion, but more so the general sense of defining types in terms of one another. The closest thing I could find was a mutual .. end block but it's possible something else exists for this purpose

[Arthur Adjedj]

Structure are supposed to be non-recursive, and rely on this property for important things like eta-expansion. In your example above, t2 is recursive, and wouldn't be accepted as a structure even if it was "inlined":

structure t2 where
  k : Option t2 --unknown identifier 't2'
  v : Nat

[Bhakti Shah]

That makes sense, thanks!

[Mac Malone]

@Bhakti Shah It is worth noting that you can essentially achieve your original example with a workaround:

structure t2_ (t1) where
k : t1
v : Nat

inductive t1 where
| C1
| C2_ (a : t2_ t1)

abbrev t2 := t2_ t1
abbrev t1.C2 (a : t2) := C2_ a