|
9 | 9 | "name": "stdout",
|
10 | 10 | "output_type": "stream",
|
11 | 11 | "text": [
|
12 |
| - "[(<CodeType.Declaration: 0>, \"Int'' : Type\\nInt'' = (a : Type) -> (a -> a) -> a -> a\")]:let\n", |
13 |
| - "Int'' : Type\n", |
14 |
| - "Int'' = (a : Type) -> (a -> a) -> a -> a(:protocol-version 1 0)\n", |
15 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 2 9) (:end 2 12)) ((:decor :type) (:type Type) (:doc-overview The type of types) (:name Type)))))) 0)\n", |
16 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 2 1) (:end 2 5)) ((:name Int'') (:implicit :False) (:key AAAAAAAAAAAFSW50Jyc=) (:decor :function) (:doc-overview ) (:type Type)))))) 0)\n", |
17 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 3 1) (:end 3 5)) ((:name Int'') (:implicit :False) (:key AAAAAAAAAAAFSW50Jyc=) (:decor :function) (:doc-overview ) (:type Type)))))) 0)\n", |
18 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 3 10) (:end 3 10)) ((:name a) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 3 14) (:end 3 17)) ((:decor :type) (:type Type) (:doc-overview The type of types) (:name Type))) (((:filename (input)) (:start 3 24) (:end 3 24)) ((:name a) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 3 29) (:end 3 29)) ((:name a) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 3 35) (:end 3 35)) ((:name a) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 3 40) (:end 3 40)) ((:name a) (:decor :bound) (:implicit :False)))))) 0)\n", |
19 |
| - "(:return (:ok defined) 0)\n", |
20 |
| - "\n", |
21 | 12 | "defined"
|
22 | 13 | ]
|
23 | 14 | }
|
|
36 | 27 | },
|
37 | 28 | {
|
38 | 29 | "cell_type": "code",
|
39 |
| - "execution_count": 3, |
| 30 | + "execution_count": 2, |
40 | 31 | "metadata": {},
|
41 | 32 | "outputs": [
|
42 | 33 | {
|
43 | 34 | "name": "stdout",
|
44 | 35 | "output_type": "stream",
|
45 | 36 | "text": [
|
46 |
| - "[(<CodeType.Undeclare: 3>, 'zero'), (<CodeType.Undeclare: 3>, 'successor'), (<CodeType.Declaration: 0>, \"zero : Int''\\nzero a = const id\\n\\n\\nsuccessor : Int'' -> Int''\\nsuccessor n a f = f . (n a f)\")]:unlet zero : Int''\n", |
47 |
| - "zero a = const id\n", |
48 |
| - "\n", |
49 |
| - "\n", |
50 |
| - "successor : Int'' -> Int''\n", |
51 |
| - "successor n a f = f . (n a f)(:return (:ok Undefined zero. ((10 4 ((:name zero) (:implicit :False) (:key AAAAAAAAAAAEemVybw==))))) 0)\n", |
52 |
| - "\n", |
53 |
| - "Undefined zero.:unlet zero : Int''\n", |
54 |
| - "zero a = const id\n", |
55 |
| - "\n", |
56 |
| - "\n", |
57 |
| - "successor : Int'' -> Int''\n", |
58 |
| - "successor n a f = f . (n a f)(:return (:ok Undefined successor. ((10 9 ((:name successor) (:implicit :False) (:key AAAAAAAAAAAJc3VjY2Vzc29y))))) 0)\n", |
59 |
| - "\n", |
60 |
| - "Undefined successor.:let\n", |
61 |
| - "zero : Int''\n", |
62 |
| - "zero a = const id\n", |
63 |
| - "\n", |
64 |
| - "\n", |
65 |
| - "successor : Int'' -> Int''\n", |
66 |
| - "successor n a f = f . (n a f)(:output (:ok (:highlight-source ((((:filename (input)) (:start 2 8) (:end 2 12)) ((:name Int'') (:implicit :False) (:key AAAAAAAAAAAFSW50Jyc=) (:decor :function) (:doc-overview ) (:type Type)))))) 0)\n", |
67 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 2 1) (:end 2 4)) ((:name zero) (:implicit :False) (:key AAAAAAAAAAAEemVybw==) (:decor :function) (:doc-overview ) (:type Int'')))))) 0)\n", |
68 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 3 1) (:end 3 4)) ((:name zero) (:implicit :False) (:key AAAAAAAAAAAEemVybw==) (:decor :function) (:doc-overview ) (:type Int''))) (((:filename (input)) (:start 3 6) (:end 3 6)) ((:name a) (:decor :bound) (:implicit :False)))))) 0)\n", |
69 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 3 10) (:end 3 14)) ((:name Prelude.Basics.const) (:implicit :False) (:key AQAAAAAAAAAABWNvbnN0AAAAAAAAAAIAAAAAAAAABkJhc2ljcwAAAAAAAAAHUHJlbHVkZQ==) (:decor :function) (:doc-overview Constant function. Ignores its second argument.) (:type a -> b -> a) (:namespace Prelude.Basics))) (((:filename (input)) (:start 3 16) (:end 3 17)) ((:name Prelude.Basics.id) (:implicit :False) (:key AQAAAAAAAAAAAmlkAAAAAAAAAAIAAAAAAAAABkJhc2ljcwAAAAAAAAAHUHJlbHVkZQ==) (:decor :function) (:doc-overview Identity function.) (:type a -> a) (:namespace Prelude.Basics)))))) 0)\n", |
70 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 6 13) (:end 6 17)) ((:name Int'') (:implicit :False) (:key AAAAAAAAAAAFSW50Jyc=) (:decor :function) (:doc-overview ) (:type Type))) (((:filename (input)) (:start 6 22) (:end 6 26)) ((:name Int'') (:implicit :False) (:key AAAAAAAAAAAFSW50Jyc=) (:decor :function) (:doc-overview ) (:type Type)))))) 0)\n", |
71 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 6 1) (:end 6 9)) ((:name successor) (:implicit :False) (:key AAAAAAAAAAAJc3VjY2Vzc29y) (:decor :function) (:doc-overview ) (:type Int'' -> Int'')))))) 0)\n", |
72 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 7 1) (:end 7 9)) ((:name successor) (:implicit :False) (:key AAAAAAAAAAAJc3VjY2Vzc29y) (:decor :function) (:doc-overview ) (:type Int'' -> Int''))) (((:filename (input)) (:start 7 11) (:end 7 11)) ((:name n) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 7 13) (:end 7 13)) ((:name a) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 7 15) (:end 7 15)) ((:name f) (:decor :bound) (:implicit :False)))))) 0)\n", |
73 |
| - "(:output (:ok (:highlight-source ((((:filename (input)) (:start 7 19) (:end 7 19)) ((:name f) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 7 21) (:end 7 21)) ((:name Prelude.Basics..) (:implicit :False) (:key AQAAAAAAAAAAAS4AAAAAAAAAAgAAAAAAAAAGQmFzaWNzAAAAAAAAAAdQcmVsdWRl) (:decor :function) (:doc-overview Function composition) (:type (b -> c) -> (a -> b) -> a -> c) (:namespace Prelude.Basics))) (((:filename (input)) (:start 7 24) (:end 7 24)) ((:name n) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 7 26) (:end 7 26)) ((:name a) (:decor :bound) (:implicit :False))) (((:filename (input)) (:start 7 28) (:end 7 28)) ((:name f) (:decor :bound) (:implicit :False)))))) 0)\n", |
74 |
| - "(:return (:ok defined) 0)\n", |
75 |
| - "\n", |
76 | 37 | "defined"
|
77 | 38 | ]
|
78 | 39 | }
|
|
86 | 47 | "successor n a f = f . (n a f)"
|
87 | 48 | ]
|
88 | 49 | },
|
| 50 | + { |
| 51 | + "cell_type": "code", |
| 52 | + "execution_count": 26, |
| 53 | + "metadata": {}, |
| 54 | + "outputs": [ |
| 55 | + { |
| 56 | + "name": "stdout", |
| 57 | + "output_type": "stream", |
| 58 | + "text": [ |
| 59 | + "4 : Int" |
| 60 | + ] |
| 61 | + } |
| 62 | + ], |
| 63 | + "source": [ |
| 64 | + "successor (successor zero) Int (*2) 1" |
| 65 | + ] |
| 66 | + }, |
89 | 67 | {
|
90 | 68 | "cell_type": "markdown",
|
91 | 69 | "metadata": {},
|
|
95 | 73 | },
|
96 | 74 | {
|
97 | 75 | "cell_type": "code",
|
98 |
| - "execution_count": 29, |
| 76 | + "execution_count": 3, |
99 | 77 | "metadata": {},
|
100 | 78 | "outputs": [
|
101 | 79 | {
|
|
118 | 96 | },
|
119 | 97 | {
|
120 | 98 | "cell_type": "code",
|
121 |
| - "execution_count": 32, |
| 99 | + "execution_count": 4, |
122 | 100 | "metadata": {},
|
123 | 101 | "outputs": [
|
124 | 102 | {
|
|
142 | 120 | },
|
143 | 121 | {
|
144 | 122 | "cell_type": "code",
|
145 |
| - "execution_count": 35, |
| 123 | + "execution_count": 5, |
146 | 124 | "metadata": {},
|
147 | 125 | "outputs": [
|
148 | 126 | {
|
|
164 | 142 | "exponent m n a = n (a -> a) $ m a"
|
165 | 143 | ]
|
166 | 144 | },
|
| 145 | + { |
| 146 | + "cell_type": "code", |
| 147 | + "execution_count": 15, |
| 148 | + "metadata": {}, |
| 149 | + "outputs": [ |
| 150 | + { |
| 151 | + "name": "stdout", |
| 152 | + "output_type": "stream", |
| 153 | + "text": [ |
| 154 | + "256 : Int" |
| 155 | + ] |
| 156 | + } |
| 157 | + ], |
| 158 | + "source": [ |
| 159 | + "to_int $ exponent (from_int 2) (from_int 8)" |
| 160 | + ] |
| 161 | + }, |
167 | 162 | {
|
168 | 163 | "cell_type": "markdown",
|
169 | 164 | "metadata": {},
|
|
173 | 168 | },
|
174 | 169 | {
|
175 | 170 | "cell_type": "code",
|
176 |
| - "execution_count": 38, |
| 171 | + "execution_count": 6, |
177 | 172 | "metadata": {},
|
178 | 173 | "outputs": [
|
179 | 174 | {
|
|
198 | 193 | },
|
199 | 194 | {
|
200 | 195 | "cell_type": "code",
|
201 |
| - "execution_count": 40, |
| 196 | + "execution_count": 7, |
202 | 197 | "metadata": {},
|
203 | 198 | "outputs": [
|
204 | 199 | {
|
|
229 | 224 | },
|
230 | 225 | {
|
231 | 226 | "cell_type": "code",
|
232 |
| - "execution_count": 41, |
| 227 | + "execution_count": 8, |
233 | 228 | "metadata": {},
|
234 | 229 | "outputs": [
|
235 | 230 | {
|
|
257 | 252 | },
|
258 | 253 | {
|
259 | 254 | "cell_type": "code",
|
260 |
| - "execution_count": 42, |
| 255 | + "execution_count": 9, |
261 | 256 | "metadata": {},
|
262 | 257 | "outputs": [
|
263 | 258 | {
|
|
288 | 283 | },
|
289 | 284 | {
|
290 | 285 | "cell_type": "code",
|
291 |
| - "execution_count": 43, |
| 286 | + "execution_count": 10, |
292 | 287 | "metadata": {},
|
293 | 288 | "outputs": [
|
294 | 289 | {
|
|
319 | 314 | },
|
320 | 315 | {
|
321 | 316 | "cell_type": "code",
|
322 |
| - "execution_count": 44, |
| 317 | + "execution_count": 11, |
323 | 318 | "metadata": {},
|
324 | 319 | "outputs": [
|
325 | 320 | {
|
|
340 | 335 | },
|
341 | 336 | {
|
342 | 337 | "cell_type": "code",
|
343 |
| - "execution_count": 47, |
| 338 | + "execution_count": 12, |
344 | 339 | "metadata": {},
|
345 | 340 | "outputs": [
|
346 | 341 | {
|
|
364 | 359 | },
|
365 | 360 | {
|
366 | 361 | "cell_type": "code",
|
367 |
| - "execution_count": 48, |
| 362 | + "execution_count": 13, |
368 | 363 | "metadata": {},
|
369 | 364 | "outputs": [
|
370 | 365 | {
|
|
0 commit comments