structure in mutually inductive type

Stream: new members

[Kris Brown]

My basic understanding is that there are conveniences that come along with declaring a type with one constructor as a structure. Is it possible to declare one of the types in a mutually-inductive declaration to be structure too? Here's a MWE

mutual inductive sumtype, A
 with sumtype : Type
  | fromA :A → sumtype
  | fromInt : ℕ → sumtype
 with A : Type                 -- how to say this is a structure?
  | mk : sumtype → A

open sumtype
#check fromA (A.mk (fromInt 0))

[Chris B]

Unfortunately no, the other half of the buy-in to structure is that it can't be recursive.

[Kris Brown]

As a follow up, is this inductive type recursive in some sense? I can't get a structure analogue to work.

def f (x: nat) :Type :=  if x = 0 then bool else nat

inductive Foo : Type → Type
   | mk (x: nat):  Foo (f x)

structure Foo' : Type → Type := (x: nat)  -- something like this