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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
module Encoded.Arith
import Encoded.Bool
import Encoded.Pair
import Term.Syntax
export
rec : {ty : Ty} -> Term (N ~> ty ~> (N * ty ~> ty) ~> ty) ctx
rec = Abs $ Abs $ Abs $
let n = Var $ There $ There Here in
let z = Var $ There Here in
let s = Var Here in
let
p : Term (N * ty) (ctx :< N :< ty :< (N * ty ~> ty))
p = Rec n
(App pair [<Zero, z])
(Abs' (\p =>
App pair
[<Suc (App fst [<p])
, App (shift s) [<p]]))
in
App snd [<p]
export
plus : Term (N ~> N ~> N) ctx
plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .)))
export
pred : Term (N ~> N) ctx
-- pred = Abs' (\n => App rec [<n, Zero, fst])
pred = Abs'
(\n => App
(Rec n
(Const Zero)
(Abs' (\f =>
Rec (App f [<Zero])
(Abs' (\k => Rec k (Suc Zero) (Const Zero)))
(Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
[<Lit 1])
export
minus : Term (N ~> N ~> N) ctx
minus = Abs $ Abs $
let m = Var $ There Here in
let n = Var Here in
Rec n m pred
export
mult : Term (N ~> N ~> N) ctx
mult = Abs' (\n =>
Rec n
(Const Zero)
(Abs $ Abs $
let f = Var $ There Here in
let m = Var Here in
App plus [<m, App f [<m]]))
export
lte : Term (N ~> N ~> B) ctx
lte = Abs' (\m => isZero . App minus [<m])
export
equal : Term (N ~> N ~> B) ctx
equal = Abs $ Abs $
let m = Var $ There Here in
let n = Var Here in
App and [<App lte [<m, n], App lte [<n, m]]
export
divmod : Term (N ~> N ~> N * N) ctx
divmod = Abs $ Abs $
let n = Var (There Here) in
let d = Var Here in
Rec
n
(App pair [<Zero, Zero])
(Abs' (\p =>
App if'
[<App lte [<shift d, App snd [<p]]
, App pair [<Suc (App fst [<p]), Zero]
, App mapSnd [<Abs' Suc, p]]))
|
