summaryrefslogtreecommitdiff
path: root/src/Encoded/Bool.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Encoded/Bool.idr')
-rw-r--r--src/Encoded/Bool.idr10
1 files changed, 0 insertions, 10 deletions
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,6 +1,5 @@
module Encoded.Bool
-import Term.Semantics
import Term.Syntax
export
@@ -8,15 +7,6 @@ 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