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

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

diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 32bb06c..42adde5 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -2,24 +2,12 @@ module Encoded.Pair
 
 import Encoded.Bool
 import Encoded.Union
-import Term.Semantics
 import Term.Syntax
 
 export
 (*) : Ty -> Ty -> Ty
 ty1 * ty2 = B ~> (ty1 <+> ty2)
 
-export
-[ShowPair]
-{ty1, ty2 : Ty} ->
-Show (TypeOf ty1) =>
-Show (TypeOf ty2) =>
-Show (TypeOf (ty1 * ty2)) where
-  show f = fastConcat
-    [ "(", show (sem prL [<] (f $ sem True [<]))
-    , ", ", show (sem prR [<] (f $ sem False [<]))
-    , ")"]
-
 export
 pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
 pair = Abs $ Abs $ Abs $
-- 
cgit v1.2.3