Stream: math-comp users

Topic: What would be mathcomp eqiivalent of decidable Prop?


view this post on Zulip walker (Nov 19 2022 at 09:52):

I am trying to have some lemmas with (P: T1 -> Prop) and (R: T1 -> T2 -> Prop) and some of those lemmas also assume that P and Q should be decidable, which kind of means P and Q can be refleced to functions that return bool, but I wanted to know what would be the correct pattern to have those assumptions ?

Lemmas usually have to flavors:

1- if P x is decidable then map P some_data_structure followed by and-ing all the results is also decidable

2- not custom_forall x, P x<-> custom_exists y, ~ P y.


Last updated: Feb 08 2023 at 07:02 UTC