## Stream: general

### Topic: invalid occurrence of recursive arg

#### Reid Barton (Jan 13 2019 at 07:42):

What does this error message mean and is there a workaround?

universe v
variables {α : Type v}
inductive closure (φ : set α → set α) : α → Prop
| clos : ∀ {t : set α}, (∀ x, t x → closure x) → ∀ x, φ t x → closure x
-- error: invalid occurrence of recursive arg#5 of 'closure.clos', the body of the functional type depends on it.


#### Reid Barton (Jan 13 2019 at 08:21):

I guess I can just use the impredicative definition

#### Kenny Lau (Jan 13 2019 at 08:25):

what is the impredicative definition?

#### Reid Barton (Jan 13 2019 at 08:35):

The intersection of all the closed subsets of α

#### Reid Barton (Jan 13 2019 at 08:47):

def closure (φ : set α → set α) : set α := ⋂₀ {s | ∀ t, t ⊆ s → φ t ⊆ s}

#### Gabriel Ebner (Jan 13 2019 at 09:00):

FTFY:

inductive closure (φ : set α → set α) : α → Prop
| clos : ∀ {t : set α}, ∀ x, (∀ x, t x → closure x) → φ t x → closure x


#### Gabriel Ebner (Jan 13 2019 at 09:03):

Lean is a bit picky about the order of the arguments to constructors. A long time ago, you couldn't even write | node : tree → α → tree → tree (you had to write α at the beginning and not in the middle).

#### Reid Barton (Jan 13 2019 at 09:05):

Interesting, thanks!

Last updated: May 14 2021 at 13:24 UTC