1 files changed, 22 insertions, 0 deletions
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))