blob: 4dd3e10b596079c207e82e26d4efba3e1fde09a0 (
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
|
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
lte : Term (N ~> N ~> B) ctx
lte = Abs' (\m => isZero . App (Op 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]]
|
