From c854bb898e90491324430626e42c381fc5f17e85 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Sat, 25 Nov 2023 14:49:38 -0600
Subject: [PATCH] fix(NonEmpty): hide the pseudo 'tail'

---
 src/Mugen/Data/NonEmpty.agda | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Mugen/Data/NonEmpty.agda b/src/Mugen/Data/NonEmpty.agda
index 703c12a..091f578 100644
--- a/src/Mugen/Data/NonEmpty.agda
+++ b/src/Mugen/Data/NonEmpty.agda
@@ -17,9 +17,10 @@ head : List⁺ A → A
 head [ x ] = x
 head (x ∷ xs) = x
 
-tail : List⁺ A → List⁺ A
-tail [ x ] = [ x ]
-tail (x ∷ xs) = xs
+private
+  tail : List⁺ A → List⁺ A
+  tail [ x ] = [ x ]
+  tail (x ∷ xs) = xs
 
 []-inj : ∀ {x y : A} → [ x ] ≡ [ y ] → x ≡ y
 []-inj p = ap head p