<div dir="ltr">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.<div><br>
</div><div><div>module Cactus where</div><div><br></div><div>open import Function</div><div>open import Data.Maybe</div><div>            </div><div>data Partial {A : Set} (P : A → Set) (Q : Set) : Maybe A → Set where</div>
<div>  Just : ∀ {x} → P x → Partial P Q (just x)</div><div>  Nothing : Q → Partial P Q nothing</div><div><br></div><div>Partial-Just : ∀ {A P Q x} → Partial {A} P Q (just x) → P x</div><div>Partial-Just (Just P) = P</div>
<div><br></div><div>Partial-Nothing : ∀ {A P Q} → Partial {A} P Q nothing → Q</div><div>Partial-Nothing (Nothing Q) = Q</div><div><br></div><div>Partial1 : {A : Set} (P : A → Set) (Q : Set) → Maybe A → Set</div><div>Partial1 = maybe</div>
<div><br></div><div>Partial1-Just : ∀ {A P Q x} → Partial1 {A} P Q (just x) → P x</div><div>Partial1-Just = id</div><div><br></div><div>Partial1-Nothing : ∀ {A P Q} → Partial1 {A} P Q nothing → Q</div><div>Partial1-Nothing = id</div>
</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Apr 27, 2013 at 9:47 AM, Dr. ERDI Gergo <span dir="ltr">&lt;<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I needed the following definition for something I&#39;ve been playing around with:<br>
<br>
  data Partial {A : Set} (P : A → Set) (Q : Set) : Maybe A → Set where<br>
    Just : ∀ {x} → P x → Partial P Q (just x)<br>
    Nothing : Q → Partial P Q nothing<br>
<br>
  Partial-Just : ∀ {A P Q x} → Partial {A} P Q (just x) → P x<br>
  Partial-Just (Just P) = P<br>
<br>
  Partial-Nothing : ∀ {A P Q} → Partial {A} P Q nothing → Q<br>
  Partial-Nothing (Nothing Q) = Q<br>
<br>
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?<br>

<br>
Thanks,<br>
        Gergo<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
<br>
  .--= ULLA! =-----------------.<br>
   \     <a href="http://gergo.erdi.hu" target="_blank">http://gergo.erdi.hu</a>   \<br>
    `---= <a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a> =-------&#39;<br>
Speak the truth, but leave immediately after.</font></span><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>