From 0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 Jun 2023 16:05:44 +0100
Subject: Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.
---
 src/Encoded/Bool.idr | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

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

diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index d185856..11bb894 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -1,11 +1,21 @@
 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
@@ -20,3 +30,19 @@ if' = Abs' (\b =>
   Rec b
     (Abs $ Const $ Var Here)
     (Const $ Const $ Abs $ Var Here))
+
+export
+and : Term (B ~> B ~> B) ctx
+and = Abs' (\b => App if' [<b, Id, Const False])
+
+export
+or : Term (B ~> B ~> B) ctx
+or = Abs' (\b => App if' [<b, Const True, Id])
+
+export
+not : Term (B ~> B) ctx
+not = Abs' (\b => App if' [<b, False, True])
+
+export
+isZero : Term (N ~> B) ctx
+isZero = Id
-- 
cgit v1.2.3