Zulip Chat Archive

Stream: new members

Topic: structure in mutually inductive type

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip 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