[Agda] Maybe-like combinator for propositions

[Daniel Peebles]

It looks like a higher-universe maybe! Not sure it helps you if you want to
explicitly pattern match on your Partial proof, but you could just pattern
match on the underlying Maybe instead, with mine.

module Cactus where

open import Function
open import Data.Maybe

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

Partial1 : {A : Set} (P : A → Set) (Q : Set) → Maybe A → Set
Partial1 = maybe

Partial1-Just : ∀ {A P Q x} → Partial1 {A} P Q (just x) → P x
Partial1-Just = id

Partial1-Nothing : ∀ {A P Q} → Partial1 {A} P Q nothing → Q
Partial1-Nothing = id


On Sat, Apr 27, 2013 at 9:47 AM, Dr. ERDI Gergo <gergo at erdi.hu> wrote:

> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130427/f0d1e40a/attachment.html