POption?

Stream: lean4

[Mac]

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]

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]

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