Zulip Chat Archive

Stream: lean4

Topic: POption?


Mac (Jul 07 2022 at 21:49):

Is there a version of Option for Prop (i.e., a POption) in the core? A quick search shows that POption itself does not exist, but I don't know whether there is some other technical term for the logical concept which it would instead be named.

Henrik Böving (Jul 07 2022 at 22:09):

Not that I am aware of I used a PSum Unit p in slimcheck to emulate it: https://github.com/leanprover-community/mathlib4/blob/ecd37441047e490ff2ad339e16f45bb8b58591bd/Mathlib/Testing/SlimCheck/Testable.lean#L93-L97.

Mario Carneiro (Jul 10 2022 at 06:13):

It has been referred to as Semidecidable in discussions in the past, although I don't think we ever made a proper definition and theory for it


Last updated: Dec 20 2023 at 11:08 UTC