From 9de870fb205fda5d8de9989e34bb39a37fcb6ed4 Mon Sep 17 00:00:00 2001
From: xenia <xenia.agda@gmail.com>
Date: Sat, 9 Sep 2023 11:46:18 +0200
Subject: [PATCH] Add list-to-list+?

---
 src/NonEmpty.agda | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda
index bad9e67..49abf3f 100644
--- a/src/NonEmpty.agda
+++ b/src/NonEmpty.agda
@@ -36,6 +36,14 @@ vec-to-list⁺ : {A : Type} → {n : ℕ} → V.Vec A (suc n) → List⁺ A
 vec-to-list⁺ (x V.∷ V.[]) = [ x ]⁺
 vec-to-list⁺ (x V.∷ xs@(_ V.∷ _)) = x ∷⁺ vec-to-list⁺ xs
 
+list-to-list⁺? : {A : Type} → List A → Maybe (List⁺ A)
+list-to-list⁺? [] = cake
+list-to-list⁺? (x ∷ xs) = real (cons⁺ x xs)
+  where
+    cons⁺ : {A : Type} → A → List A → List⁺ A
+    cons⁺ a [] = [ a ]⁺
+    cons⁺ a (x ∷ xs) = a ∷⁺ cons⁺ x xs
+
 instance
   ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A)
   ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺"