From 6507dfe9325ab7eaee1c0836fc14d507bc644b42 Mon Sep 17 00:00:00 2001
From: xenia <xenia.agda@gmail.com>
Date: Sat, 9 Sep 2023 12:56:47 +0200
Subject: [PATCH] Add some append functions for List+

---
 src/NonEmpty.agda | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda
index 49abf3f..395d08a 100644
--- a/src/NonEmpty.agda
+++ b/src/NonEmpty.agda
@@ -24,6 +24,25 @@ foldl : {A B : Type} → (B → A → B) → B → List⁺ A → B
 foldl _+_ acc [ x ]⁺ = acc + x
 foldl _+_ acc (x ∷⁺ xs) = foldl _+_ (acc + x) xs
 
+cons⁺ : {A : Type} → A → List A → List⁺ A
+cons⁺ a [] = [ a ]⁺
+cons⁺ a (x ∷ xs) = a ∷⁺ cons⁺ x xs
+
+_⁺++⁺_ : {A : Type} → List⁺ A → List⁺ A → List⁺ A
+[ x ]⁺ ⁺++⁺ l₁ = x ∷⁺ l₁
+(x ∷⁺ l₀) ⁺++⁺ l₁ = x ∷⁺ (l₀ ⁺++⁺ l₁)
+
+_++⁺_ : {A : Type} → List A → List⁺ A → List⁺ A
+[] ++⁺ l₁ = l₁
+(x ∷ l₀) ++⁺ l₁ = x ∷⁺ (l₀ ++⁺ l₁)
+
+_⁺++_ : {A : Type} → List⁺ A → List A → List⁺ A
+[ x ]⁺ ⁺++ [] = [ x ]⁺
+[ x ]⁺ ⁺++ (y ∷ l₁) = (x ∷⁺ [ y ]⁺ ) ⁺++ l₁
+(x ∷⁺ l₀) ⁺++ l₁ = x ∷⁺ (l₀ ⁺++ l₁)
+
+infixr 20 _⁺++⁺_ _++⁺_ _⁺++_
+
 list⁺-to-list : {A : Type} → List⁺ A → List A
 list⁺-to-list [ x ]⁺ = x ∷ []
 list⁺-to-list (x ∷⁺ xs) = x ∷ list⁺-to-list xs
@@ -39,10 +58,7 @@ 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)