blob: 778f65ddf0b2983e9f4835884233330673fdd5d6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
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))
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
|
