Stream: new members
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