The first two of those are already in the lib (but I agree they&#39;re kinda hard to find):<div><br></div><div><a href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Product.html#394">http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Product.html#394</a><br>
</div><div><a href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Sum.html#513">http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Sum.html#513</a><br></div><div><br></div><div>The others might be too, but I haven&#39;t seen them :)</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Nov 23, 2012 at 4:36 AM, Peter Divianszky <span dir="ltr">&lt;<a href="mailto:divipp@gmail.com" target="_blank">divipp@gmail.com</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>
What is the way to add definitions to Standard Libraries?<br>
<br>
I would like to add the following if you find it useful:<br>
<br>
<br>
---------- Relation.Nullary<br>
<br>
_∧_ : {A B : Set} → Dec A → Dec B → Dec (A × B)<br>
no ¬p ∧ _     = no (¬p ∘f proj₁)<br>
_     ∧ no ¬p = no (¬p ∘f proj₂)<br>
yes a ∧ yes b = yes (a , b)<br>
<br>
_∨_ : {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)<br>
no ¬p ∨ no ¬q = no ([ ¬p , ¬q ]′)<br>
yes a ∨ _     = yes (inj₁ a)<br>
_     ∨ yes b = yes (inj₂ b)<br>
<br>
---------- Data.Nat.Properties<br>
<br>
to-from≤ : ∀ {n x} (y : x ≤ n) → toℕ (fromℕ≤ (s≤s y)) ≡ x<br>
to-from≤ z≤n = refl<br>
to-from≤ (s≤s y) rewrite to-from≤ y = refl<br>
<br>
---------- Data.Product<br>
<br>
syntax ∃ (λ x → P) = x ∣ P<br>
<br>
data ∃_⁻¹_ {A B : Set} (f : A → B) : B → Set where<br>
   inv : (x : A) → ∃ f ⁻¹ f x<br>
<br>
infix 9 ∃_⁻¹_<br>
<br>
----------<br>
<br>
Should I include use cases?<br>
<br>
By the way, the following is not possible but would be nice:<br>
<br>
f : y ∣ P → ... y ...<br>
<br>
<br>
Cheers,<br>
Peter<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>