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
|
(\X =>
[ Var: Nat
, Zero: <>
, Suc: X
, Rec: <Target: X, Zero: X, Suc: X>
, Abs: X
, App: <Fun: X, Arg: X>
])
->
(\X =>
[ Var: Nat
, Lit: Nat
, Suc: X
, Abs: X
, App: <Fun: X, Arg: X>
, Unit: <>
, Pair: <Fst: X, Snd: X>
, Fst: X
, Snd: X
, Absurd: <Target: X>
, Inl: X
, Inr: X
, Case: <Target: X, Left: X, Right: X>
, Expand: X
, Contract: X
, Fold: <Target: X, Body: X>
, Let: <Bound: X, Body: X>
, Annot:
< Term: X
, Type: (\Y =>
[ Var: Nat
, N: <>
, Arrow: <Dom: Y, Cod: Y>
, Unit: <>
, Pair: <Fst: Y, Snd: Y>
, Bottom: <>
, Sum: <Left: Y, Right: Y>
, Fix: Y
])
>
])
|
