diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-16 18:01:33 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-16 18:01:33 +0100 |
| commit | af7c222cc3e487cd3ca8b5dd8749b7e258da7c7c (patch) | |
| tree | 995c3a9d7bc6965d2de56b8a4e1f3f10376e6e86 /src/Encoded/Bool.idr | |
| parent | 5adc1ae9357e42937a601aab57d16b2190e10536 (diff) | |
Define semantics and encode types up to pairs.
Diffstat (limited to 'src/Encoded/Bool.idr')
| -rw-r--r-- | src/Encoded/Bool.idr | 22 |
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)) |