Stream: Coq users

Topic: Canonical name for always-true predicate


view this post on Zulip Karl Palmskog (May 18 2022 at 07:59):

Is it really best practice to write out fun _ => True every time one wants an always-true one-place predicate? Shouldn't there be some canonical name? I tried grepping through stdlib and stdpp to no avail.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 08:01):

there's Program.Basics.const

view this post on Zulip Karl Palmskog (May 18 2022 at 08:02):

but that's a two-place predicate, right? Or it returns Type.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 08:03):

it's Definition const {A B} (a : A) := fun _ : B => a.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 08:04):

however it's univ monomorphic so using it everywhere may have "fun" results

view this post on Zulip Karl Palmskog (May 18 2022 at 08:06):

ah, that's a bit more than I'd normally bargain for, but thanks.

view this post on Zulip Ali Caglayan (May 18 2022 at 11:04):

There is also Ensembles.Full_set, not that I would recommend using it tho.

view this post on Zulip Alexander Gryzlov (May 19 2022 at 18:25):

mathcomp uses predT for fun=>true, we also define a Prop-level PredT in fcsl-pcm: https://github.com/imdea-software/fcsl-pcm/blob/master/core/pred.v#L84


Last updated: Feb 06 2023 at 12:04 UTC