From af7c222cc3e487cd3ca8b5dd8749b7e258da7c7c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 16 Jun 2023 18:01:33 +0100
Subject: Define semantics and encode types up to pairs.

---
 src/Encoded/Bool.idr | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 src/Encoded/Bool.idr

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

diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
new file mode 100644
index 0000000..d185856
--- /dev/null
+++ b/src/Encoded/Bool.idr
@@ -0,0 +1,22 @@
+module Encoded.Bool
+
+import Term.Syntax
+
+export
+B : Ty
+B = N
+
+export
+True : Term B ctx
+True = Lit 0
+  
+export
+False : Term B ctx
+False = Lit 1
+
+export
+if' : Term (B ~> ty ~> ty ~> ty) ctx
+if' = Abs' (\b =>
+  Rec b
+    (Abs $ Const $ Var Here)
+    (Const $ Const $ Abs $ Var Here))
-- 
cgit v1.2.3