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.++ "⁺"