fix(NonEmpty): hide the pseudo 'tail'

RedPRL · Nov 25, 2023 · c854bb8 · c854bb8
1 parent 678da16
commit c854bb8
Showing 1 changed file with 4 additions and 3 deletions.
diff --git 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