[Agda] StdLib additions

[Daniel Peebles]

The first two of those are already in the lib (but I agree they're kinda
hard to find):

http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Product.html#394
http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Sum.html#513

The others might be too, but I haven't seen them :)


On Fri, Nov 23, 2012 at 4:36 AM, Peter Divianszky <divipp at gmail.com> wrote:

> Hi,
>
> What is the way to add definitions to Standard Libraries?
>
> I would like to add the following if you find it useful:
>
>
> ---------- Relation.Nullary
>
> _∧_ : {A B : Set} → Dec A → Dec B → Dec (A × B)
> no ¬p ∧ _     = no (¬p ∘f proj₁)
> _     ∧ no ¬p = no (¬p ∘f proj₂)
> yes a ∧ yes b = yes (a , b)
>
> _∨_ : {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
> no ¬p ∨ no ¬q = no ([ ¬p , ¬q ]′)
> yes a ∨ _     = yes (inj₁ a)
> _     ∨ yes b = yes (inj₂ b)
>
> ---------- Data.Nat.Properties
>
> to-from≤ : ∀ {n x} (y : x ≤ n) → toℕ (fromℕ≤ (s≤s y)) ≡ x
> to-from≤ z≤n = refl
> to-from≤ (s≤s y) rewrite to-from≤ y = refl
>
> ---------- Data.Product
>
> syntax ∃ (λ x → P) = x ∣ P
>
> data ∃_⁻¹_ {A B : Set} (f : A → B) : B → Set where
>    inv : (x : A) → ∃ f ⁻¹ f x
>
> infix 9 ∃_⁻¹_
>
> ----------
>
> Should I include use cases?
>
> By the way, the following is not possible but would be nice:
>
> f : y ∣ P → ... y ...
>
>
> Cheers,
> Peter
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121123/5ec9b0f9/attachment.html