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/Fin.idr | 5 -----
 1 file changed, 5 deletions(-)

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

diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
index 901c612..0029760 100644
--- a/src/Encoded/Fin.idr
+++ b/src/Encoded/Fin.idr
@@ -5,7 +5,6 @@ import public Data.Nat
 import Data.Stream
 import Encoded.Arith
 import Encoded.Pair
-import Term.Semantics
 import Term.Syntax
 
 export
@@ -39,10 +38,6 @@ export
 forget : Term (Fin k ~> N) ctx
 forget = Id
 
-export
-allSem : (k : Nat) -> List (TypeOf (Fin k))
-allSem k = take k nats
-
 export
 divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
 divmod' k = Abs' (\n => App divmod [<n, Lit k])
-- 
cgit v1.2.3