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