Definition of an inductive type

Stream: new members

[nemo]

I want to define an inductive type like this

import Mathlib
inductive MyStruct (α : Type*) where
  | base : α → MyStruct α
  | succ : Finset (MyStruct α) → MyStruct α

which failed since Finset (MyStruct α) contains a non-possitive occurence of MyStruct α.

But by my intuition, this should be a well-defined inductive type.

So how can I define it in a correct way?

[Aaron Liu]

You want hereditarily finite sets with α as atoms?

[Kenny Lau]

you'll have to manually construct it

[Aaron Liu]

you may be interested in #combinatorial-games > Loopy games @ 💬

[Kenny Lau]

you might be interested to see how docs#ZFSet is defined as a quotient of docs#PSet

[nemo]

Kenny Lau said:

you might be interested to see how docs#ZFSet is defined as a quotient of docs#PSet

So should I define it as

inductive PreMyStruct (α : Type*) where
  | base : α → PreMyStruct α
  | succ :  (List α) → PreMyStruct α

and get MyStruct as its quotient type?

[Aaron Liu]

you could do that too

[nemo]

I find it more preferable to me to use

def Finset' α := @Quotient (List α) {
  r := fun l₁ l₂ => ∀ x, x∈ l₁ ↔ x∈ l₂
  iseqv := by
    constructor
    · intros;rfl
    · intro _ _ f;simp[f]
    · intro _ _ _ f;simp[f]
}
inductive MyStruct (α : Type*) where
  | base : α → MyStruct α
  | succ :  (Finset' α) → MyStruct α

thank y'all for your help

[Aaron Liu]

You've changed it to be nonrecursive

[nemo]

Ouch！How careless I was. That didn't really solve the problem