[ add ] more properties of Data.List.Relation.Unary.All.Null

CHANGELOG.md

@@ -423,6 +423,13 @@ Additions to existing modules
            ∃[ xs ] Appending as bs xs × Appending xs cs ds
   ```
 
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  ¬Null-∷         : ¬ Null (x ∷ xs)
+  Null?           : Decidable Null
+  Null-irrelevant : Irrelevant Null
+  ```
+
 * In `Data.Nat.DivMod`:
   ```agda
   m<suc[m/n]*n : ∀ m n → m < suc (m / n) * n

src/Data/List/Relation/Unary/All/Properties.agda

@@ -47,7 +47,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
 open import Relation.Unary
-  using (Decidable; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Irrelevant; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private
@@ -62,6 +62,7 @@ private
     x y : A
     xs ys : List A
 
+
 ------------------------------------------------------------------------
 -- Re-export Core Properties
 
@@ -74,8 +75,17 @@ Null⇒null : Null xs → T (null xs)
 Null⇒null [] = _
 
 null⇒Null : T (null xs) → Null xs
-null⇒Null {xs = []   } _ = []
-null⇒Null {xs = _ ∷ _} ()
+null⇒Null {xs = []} _ = []
+
+¬Null-∷ : ¬ Null (x ∷ xs)
+¬Null-∷ (() ∷ _)
+
+Null? : Decidable (Null {A = A})
+Null? []      = yes []
+Null? (_ ∷ _) = no ¬Null-∷
+
+Null-irrelevant : Irrelevant (Null {A = A})
+Null-irrelevant [] [] = refl
 
 ------------------------------------------------------------------------
 -- Properties of the "points-to" relation _[_]=_