Karl Palmskog (May 18 2022 at 07:59): 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.
Gaëtan Gilbert (May 18 2022 at 08:01):there's Program.Basics.const
Karl Palmskog (May 18 2022 at 08:02):but that's a two-place predicate, right? Or it returns Type.
Gaëtan Gilbert (May 18 2022 at 08:03):it's Definition const {A B} (a : A) := fun _ : B => a.
Gaëtan Gilbert (May 18 2022 at 08:04):however it's univ monomorphic so using it everywhere may have "fun" results
Karl Palmskog (May 18 2022 at 08:06):ah, that's a bit more than I'd normally bargain for, but thanks.
Ali Caglayan (May 18 2022 at 11:04):There is also Ensembles.Full_set, not that I would recommend using it tho.
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: Sep 26 2023 at 11:01 UTC