fixed_points vs is_fixed_pt

Stream: general

[Yaël Dillies]

function.fixed_points and is_fixed_point (see dynamics.fixed_points.basic) are the same thing, one as a predicate, and the other as a set. Do we really want both? It's a bit annoying to have only half of the API for each.

[Eric Wieser]

The current API looks fine to me; we have docs#function.mem_fixed_points to normalize it, and the set version is just for bundled lemmas

[Yaël Dillies]

Oh really? I would have thought we wanted only the set one because the predicate is really an underpowered version of it.

[Eric Wieser]

Oh I thought you might be advocating having only the non-set one

[Yaël Dillies]

Ah no no. I much prefer the set version.

[Yakov Pechersky]

The predicate has all sorts of dot notation based api for quick proofs

[Yury G. Kudryashov]

The main argument for is_fixed_pt is the dot notation API.

[Eric Wieser]

You could get dot notation to work on has_mem.mem with some hacky abbreviations

[Yaël Dillies]

Hmm... What's the precedent of this "predicate vs set" contention?

[Yury G. Kudryashov]

I'm not sure that hacky abbreviations will work in all cases (e.g., for functions/lemmas with many arguments).