From 6385ecf96cd60885c221e3144b5a5ec63eb5c831 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 22 Jun 2023 17:57:48 +0100
Subject: Add encodings for containers.

Remove useless junk.
---
 src/Encoded/Vect.idr | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'src/Encoded/Vect.idr')

diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr
index a427196..064de5f 100644
--- a/src/Encoded/Vect.idr
+++ b/src/Encoded/Vect.idr
@@ -6,20 +6,12 @@ import Encoded.Bool
 import Encoded.Pair
 import Encoded.Fin
 
-import Term.Semantics
 import Term.Syntax
 
 export
 Vect : Nat -> Ty -> Ty
 Vect k ty = Fin k ~> ty
 
-export
-[ShowVect]
-{k : Nat} ->
-Show (TypeOf ty) =>
-Show (TypeOf (Vect k ty)) where
-  show f = "[" ++ joinBy ", " (map (show . f) $ allSem k) ++ "]"
-
 export
 nil : {ty : Ty} -> Term (Vect 0 ty) ctx
 nil = absurd
-- 
cgit v1.2.3