Data.List.Fresh.NonEmpty (#1624)

Author: fangyi-zhou

CHANGELOG.md

@@ -342,14 +342,14 @@ Deprecated names
   sym-↔   ↦   ↔-sym
   ```
 
-* In `Data.Fin.Base`: 
-two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the position of the Fin m argument. 
+* In `Data.Fin.Base`:
+two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the position of the Fin m argument.
   ```
   inject+   ↦   flip _↑ˡ_
   raise     ↦   _↑ʳ_
   ```
 
-* In `Data.Fin.Properties`: 
+* In `Data.Fin.Properties`:
   ```
   toℕ-raise       ↦ toℕ-↑ʳ
   toℕ-inject+ n i ↦ sym (toℕ-↑ˡ i n)
@@ -358,11 +358,11 @@ two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. '
   Fin0↔⊥        ↦ 0↔⊥
   ```
 
-* In `Data.Vec.Properties`: 
+* In `Data.Vec.Properties`:
   ```
   []≔-++-inject+       ↦ []≔-++-↑ˡ
   ```
-  Additionally, `[]≔-++-↑ʳ`, by analogy. 
+  Additionally, `[]≔-++-↑ʳ`, by analogy.
 
 * In `Foreign.Haskell.Either` and `Foreign.Haskell.Pair`:
   ```
@@ -393,6 +393,11 @@ New modules
   Data.Default
   ```
 
+* A small library for a non-empty fresh list:
+  ```
+  Data.List.Fresh.NonEmpty
+  ```
+
 * Show module for unnormalised rationals:
   ```
   Data.Rational.Unnormalised.Show

src/Data/List/Fresh/NonEmpty.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A non-empty fresh list
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Fresh.NonEmpty where
+
+open import Level using (Level; _⊔_)
+open import Data.List.Fresh as List# using (List#; []; cons; fresh)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Nat using (ℕ; suc)
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary as B using (Rel)
+
+private
+  variable
+    a r : Level
+    A : Set a
+    R : Rel A r
+
+------------------------------------------------------------------------
+-- Definition
+
+infixr 5 _∷#⁺_
+
+record List#⁺ (A : Set a) (R : Rel A r) : Set (a ⊔ r) where
+  constructor _∷#⁺_
+  field
+    head : A
+    tail : List# A R
+    {rel} : fresh A R head tail
+
+open List#⁺
+
+------------------------------------------------------------------------
+-- Operations
+
+uncons : List#⁺ A R → A × List# A R
+uncons (x ∷#⁺ xs) = x , xs
+
+[_] : A → List#⁺ A R
+[ x ] = x ∷#⁺ []
+
+length : List#⁺ A R → ℕ
+length (x ∷#⁺ xs) = suc (List#.length xs)
+
+-- Conversion
+
+toList# : List#⁺ A R → List# A R
+toList# l = cons (l .head) (l .tail) (l .rel)
+
+fromList# : List# A R → Maybe (List#⁺ A R)
+fromList# []             = nothing
+fromList# (cons a as ps) = just (record { head = a ; tail = as ; rel = ps })