Zulip Chat Archive

Stream: general

Topic: invalid occurrence of recursive arg


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

view this post on Zulip Reid Barton (Jan 13 2019 at 08:21):

I guess I can just use the impredicative definition

view this post on Zulip Kenny Lau (Jan 13 2019 at 08:25):

what is the impredicative definition?

view this post on Zulip Reid Barton (Jan 13 2019 at 08:35):

The intersection of all the closed subsets of α

view this post on Zulip Reid Barton (Jan 13 2019 at 08:47):

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

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

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

view this post on Zulip Reid Barton (Jan 13 2019 at 09:05):

Interesting, thanks!


Last updated: May 14 2021 at 13:24 UTC