Upstream classes from iog-agda-prelude

Class/Allable.agda

@@ -0,0 +1,4 @@
+module Class.Allable where
+
+open import Class.Allable.Core public
+open import Class.Allable.Instance public

Class/Allable/Core.agda

@@ -0,0 +1,18 @@
+module Class.Allable.Core where
+
+open import Class.Prelude
+
+record Allable (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where
+  field All : ∀ {A} → (A → Set) → F A → Set ℓ
+
+  ∀∈-syntax   = All
+  ∀∈-syntax′  = All
+  ¬∀∈-syntax  = λ {A} P → ¬_ ∘ All {A} P
+  ¬∀∈-syntax′ = ¬∀∈-syntax
+  infix 2 ∀∈-syntax ∀∈-syntax′ ¬∀∈-syntax ¬∀∈-syntax′
+  syntax ∀∈-syntax   P         xs = ∀[∈     xs ] P
+  syntax ∀∈-syntax′  (λ x → P) xs = ∀[  x ∈ xs ] P
+  syntax ¬∀∈-syntax  P         xs = ¬∀[∈    xs ] P
+  syntax ¬∀∈-syntax′ (λ x → P) xs = ¬∀[ x ∈ xs ] P
+
+open Allable ⦃...⦄ public

Class/Allable/Instance.agda

@@ -0,0 +1,34 @@
+module Class.Allable.Instance where
+
+open import Class.Prelude
+open import Class.Allable.Core
+
+import Data.List.Relation.Unary.All as L
+import Data.Vec.Relation.Unary.All as V
+import Data.Maybe.Relation.Unary.All as M
+
+instance
+  Allable-List : Allable {ℓ} List
+  Allable-List .All = L.All
+
+  Allable-Vec : ∀ {n} → Allable {ℓ} (flip Vec n)
+  Allable-Vec .All P = V.All P
+
+  Allable-Maybe : Allable {ℓ} Maybe
+  Allable-Maybe .All = M.All
+
+private
+  open import Class.Decidable
+  open import Class.HasOrder
+
+  _ : ∀[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0
+  _ = auto
+
+  _ : ∀[ x ∈ just 42 ] x > 0
+  _ = auto
+
+  _ : ∀[ x ∈ nothing ] x > 0
+  _ = auto
+
+  _ : ¬∀[ x ∈ just 0 ] x > 0
+  _ = auto

Class/Anyable.agda

@@ -0,0 +1,4 @@
+module Class.Anyable where
+
+open import Class.Anyable.Core public
+open import Class.Anyable.Instance public

Class/Anyable/Core.agda

@@ -0,0 +1,18 @@
+module Class.Anyable.Core where
+
+open import Class.Prelude
+
+record Anyable (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where
+  field Any : ∀ {A} → (A → Set) → F A → Set ℓ
+
+  ∃∈-syntax  = Any
+  ∃∈-syntax′ = Any
+  ∄∈-syntax  = λ {A} P → ¬_ ∘ Any {A} P
+  ∄∈-syntax′ = ∄∈-syntax
+  infix 2 ∃∈-syntax ∃∈-syntax′ ∄∈-syntax ∄∈-syntax′
+  syntax ∃∈-syntax  P         xs = ∃[∈    xs ] P
+  syntax ∃∈-syntax′ (λ x → P) xs = ∃[ x ∈ xs ] P
+  syntax ∄∈-syntax  P         xs = ∄[∈    xs ] P
+  syntax ∄∈-syntax′ (λ x → P) xs = ∄[ x ∈ xs ] P
+
+open Anyable ⦃...⦄ public

Class/Anyable/Instance.agda

@@ -0,0 +1,31 @@
+module Class.Anyable.Instance where
+
+open import Class.Prelude
+open import Class.Anyable.Core
+
+import Data.List.Relation.Unary.Any as L
+import Data.Vec.Relation.Unary.Any as V
+import Data.Maybe.Relation.Unary.Any as M
+
+instance
+  Anyable-List : Anyable {ℓ} List
+  Anyable-List .Any = L.Any
+
+  Anyable-Vec : ∀ {n} → Anyable {ℓ} (flip Vec n)
+  Anyable-Vec .Any P = V.Any P
+
+  Anyable-Maybe : Anyable {ℓ} Maybe
+  Anyable-Maybe .Any = M.Any
+
+private
+  open import Class.Decidable
+  open import Class.HasOrder
+
+  _ : ∃[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0
+  _ = auto
+
+  _ : ∃[ x ∈ just 42 ] x > 0
+  _ = auto
+
+  _ : ∄[ x ∈ nothing ] x > 0
+  _ = auto

Class/Decidable/Core.agda

@@ -77,3 +77,6 @@ module _ {A B C : Type ℓ} where
 infix -100 auto∶_
 auto∶_ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Type
 auto∶_ A = True ¿ A ¿
+
+dec-✓ : ∀ {P : Type ℓ} ⦃ _ : P ⁇ ⦄ (p : P) → ∃[ p′ ] ¿ P ¿ ≡ yes p′
+dec-✓ = dec-yes ¿ _ ¿

Class/Default.agda

@@ -6,12 +6,15 @@
 module Class.Default where
 
 open import Class.Prelude
+import Data.Vec as V
 
 record Default (A : Type ℓ) : Type ℓ where
   constructor ⌞_⌟
   field def : A
 open Default ⦃...⦄ public
 
+private variable n : ℕ
+
 instance
   Default-⊤ : Default ⊤
   Default-⊤ = ⌞ tt ⌟
@@ -34,11 +37,17 @@ instance
   Default-ℤ : Default ℤ
   Default-ℤ = ⌞ ℤ.pos def ⌟
 
-  Default-Fin : ∀ {n : ℕ} → Default (Fin (suc n))
+  Default-Fin : Default (Fin (suc n))
   Default-Fin = ⌞ zero ⌟
 
   Default-List : Default (List A)
   Default-List = ⌞ [] ⌟
 
+  Default-Vec-zero : Default (Vec A 0)
+  Default-Vec-zero = ⌞ V.[] ⌟
+
+  Default-Vec-suc : ⦃ Default A ⦄ → Default (Vec A (suc n))
+  Default-Vec-suc = ⌞ V.replicate _ def ⌟
+
   Default-→ : ⦃ Default B ⦄ → Default (A → B)
   Default-→ = ⌞ const def ⌟

Class/Monoid/Instances.agda

@@ -43,6 +43,16 @@ module _ where
     instance _ = Monoid-ℕ-*
     MonoidLaws-ℕ-* = MonoidLaws≡ ℕ ∋ record {ε-identity = *-identityˡ , *-identityʳ}
 
+-- ** natural numbers
+module _ where
+  open import Data.Nat.Binary
+  open import Data.Nat.Binary.Properties
+
+  instance _ = Semigroup-ℕᵇ-+
+  Monoid-ℕᵇ-+ = Monoid ℕᵇ ∋ λ where .ε → zero
+  instance _ = Monoid-ℕᵇ-+
+  MonoidLaws-ℕᵇ-+ = MonoidLaws≡ ℕᵇ ∋ record {ε-identity = +-identityˡ , +-identityʳ}
+
 -- ** integers
 module _ where
   open import Data.Integer.Properties

Class/Prelude.agda

@@ -13,7 +13,7 @@ open import Data.Empty public
 open import Data.Unit public
   using (⊤; tt)
 open import Data.Product public
-  using (_×_; _,_; proj₁; proj₂; Σ; ∃; -,_)
+  using (_×_; _,_; proj₁; proj₂; Σ; ∃; ∃-syntax; -,_)
 open import Data.Sum public
   using (_⊎_; inj₁; inj₂)
 open import Data.Bool public

Class/Semigroup/Instances.agda

@@ -56,6 +56,16 @@ module _ where
     record {◇-assocʳ = *-assoc; ◇-comm = *-comm}
     where instance _ = Semigroup-ℕ-*
 
+-- ** binary natural numbers
+module _ where
+  open import Data.Nat.Binary
+  open import Data.Nat.Binary.Properties
+
+  Semigroup-ℕᵇ-+ = Semigroup ℕᵇ ∋ λ where ._◇_ → _+_
+  SemigroupLaws-ℕᵇ-+ = SemigroupLaws ℕᵇ _≡_ ∋
+    record {◇-assocʳ = +-assoc; ◇-comm = +-comm}
+    where instance _ = Semigroup-ℕᵇ-+
+
 -- ** integers
 module _ where
   open import Data.Integer

standard-library-classes.agda

@@ -18,6 +18,8 @@ open import Class.DecEq.WithK public
 open import Class.Decidable public
 
 -- ** Others
+open import Class.Allable public
+open import Class.Anyable public
 open import Class.Default public
 open import Class.HasAdd public
 open import Class.HasOrder public