Zulip Chat Archive

Stream: general

Topic: fixed_points vs is_fixed_pt


Yaël Dillies (Aug 15 2021 at 06:44):

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 (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: Dec 20 2023 at 11:08 UTC