## Stream: new members

### Topic: structure in mutually inductive type

#### Kris Brown (Jul 03 2020 at 03:25):

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 (Jul 03 2020 at 04:29):

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

#### Kris Brown (Jul 12 2020 at 01:10):

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


Last updated: May 08 2021 at 04:14 UTC