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

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

diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index 11bb894..778f65d 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -1,21 +1,11 @@
 module Encoded.Bool
 
-import Term.Semantics
 import Term.Syntax
 
 export
 B : Ty
 B = N
 
-export
-Show (TypeOf B) where
-  show 0 = "true"
-  show (S k) = "false"
-
-export
-toBool : TypeOf B -> Bool
-toBool = (== 0)
-
 export
 True : Term B ctx
 True = Lit 0
-- 
cgit v1.2.3