invalid occurrence of recursive arg

Stream: general

[Reid Barton]

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]

I guess I can just use the impredicative definition

[Kenny Lau]

what is the impredicative definition?

[Reid Barton]

The intersection of all the closed subsets of α

[Reid Barton]

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

[Gabriel Ebner]

FTFY:

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

[Gabriel Ebner]

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]

Interesting, thanks!