Topic: fixed_points vs is_fixed_pt
Yaël Dillies (Aug 15 2021 at 06:44):
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 (Aug 15 2021 at 08:11):
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 (Aug 15 2021 at 10:16):
Oh really? I would have thought we wanted only the set one because the predicate is really an underpowered version of it.
Eric Wieser (Aug 15 2021 at 10:19):
Oh I thought you might be advocating having only the non-set one
Yaël Dillies (Aug 15 2021 at 10:21):
Ah no no. I much prefer the set version.
Yakov Pechersky (Aug 15 2021 at 15:28):
The predicate has all sorts of dot notation based api for quick proofs
Yury G. Kudryashov (Aug 15 2021 at 15:47):
The main argument for
is_fixed_pt is the dot notation API.
Eric Wieser (Aug 15 2021 at 16:48):
You could get dot notation to work on
has_mem.mem with some hacky abbreviations
Yaël Dillies (Aug 15 2021 at 17:03):
Hmm... What's the precedent of this "predicate vs set" contention?
Yury G. Kudryashov (Aug 15 2021 at 17:05):
I'm not sure that hacky abbreviations will work in all cases (e.g., for functions/lemmas with many arguments).
Last updated: Aug 03 2023 at 10:10 UTC