-
Notifications
You must be signed in to change notification settings - Fork 2
/
huge_elab.txt
43 lines (43 loc) · 1.1 KB
/
huge_elab.txt
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
(((ann
(fn
[pair]
((ann
(fn
[p1]
((ann
(fn
[zero]
(ann
(fn [sel] ((p1 zero) sel))
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]))
[(IFn)
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]])
(ann (fn [x] x) (IFn))))
[[(IFn)
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]]
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]])
(ann
(fn [x] (pair x))
[(IFn)
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]])))
[[(IFn)
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]]
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]])
(ann
(fn
[x]
(ann
(fn [sel] ((sel x) x))
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]))
[(IFn)
:->
[[(IFn) :-> [(IFn) :-> [Int :-> Int]]] :-> [Int :-> Int]]]))
(ann
(fn [fst] (ann (fn [snd] fst) [(IFn) :-> [Int :-> Int]]))
[(IFn) :-> [(IFn) :-> [Int :-> Int]]]))