[Agda] Maybe-like combinator for propositions
Dr. ERDI Gergo
gergo at erdi.hu
Sat Apr 27 15:47:41 CEST 2013
Hi,
I needed the following definition for something I've been playing around
with:
data Partial {A : Set} (P : A → Set) (Q : Set) : Maybe A → Set where
Just : ∀ {x} → P x → Partial P Q (just x)
Nothing : Q → Partial P Q nothing
Partial-Just : ∀ {A P Q x} → Partial {A} P Q (just x) → P x
Partial-Just (Just P) = P
Partial-Nothing : ∀ {A P Q} → Partial {A} P Q nothing → Q
Partial-Nothing (Nothing Q) = Q
Apart from the horrible name, this sounds very basic. I have this feeling
something like this should already be in the standard library (possibly
some combination of `maybe` and `All` from `Data.Maybe`?). Is there a
nicer way (and a nicer name!) to do this?
Thanks,
Gergo
--
.--= ULLA! =-----------------.
\ http://gergo.erdi.hu \
`---= gergo at erdi.hu =-------'
Speak the truth, but leave immediately after.
More information about the Agda
mailing list