1{ Bool : 2 { and : ∀(xs : List Bool) → Bool 3 , build : 4 ∀(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool 5 , even : ∀(xs : List Bool) → Bool 6 , fold : 7 ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool 8 , not : ∀(b : Bool) → Bool 9 , odd : ∀(xs : List Bool) → Bool 10 , or : ∀(xs : List Bool) → Bool 11 , show : ∀(b : Bool) → Text 12 } 13, Double : { show : Double → Text } 14, Function : 15 { compose : 16 ∀(A : Type) → 17 ∀(B : Type) → 18 ∀(C : Type) → 19 ∀(f : A → B) → 20 ∀(g : B → C) → 21 ∀(x : A) → 22 C 23 , identity : ∀(a : Type) → ∀(x : a) → a 24 } 25, Integer : 26 { abs : ∀(n : Integer) → Natural 27 , add : ∀(m : Integer) → ∀(n : Integer) → Integer 28 , clamp : Integer → Natural 29 , equal : ∀(a : Integer) → ∀(b : Integer) → Bool 30 , greaterThan : ∀(x : Integer) → ∀(y : Integer) → Bool 31 , greaterThanEqual : ∀(x : Integer) → ∀(y : Integer) → Bool 32 , lessThan : ∀(x : Integer) → ∀(y : Integer) → Bool 33 , lessThanEqual : ∀(x : Integer) → ∀(y : Integer) → Bool 34 , multiply : ∀(m : Integer) → ∀(n : Integer) → Integer 35 , negate : Integer → Integer 36 , negative : ∀(n : Integer) → Bool 37 , nonNegative : ∀(n : Integer) → Bool 38 , nonPositive : ∀(n : Integer) → Bool 39 , positive : ∀(n : Integer) → Bool 40 , show : Integer → Text 41 , subtract : ∀(m : Integer) → ∀(n : Integer) → Integer 42 , toDouble : Integer → Double 43 , toNatural : ∀(n : Integer) → Optional Natural 44 } 45, JSON : 46 { Nesting : Type 47 , Tagged : ∀(a : Type) → Type 48 , Type : Type 49 , array : 50 ∀ ( x 51 : List 52 ( ∀(JSON : Type) → 53 ∀ ( json 54 : { array : List JSON → JSON 55 , bool : Bool → JSON 56 , double : Double → JSON 57 , integer : Integer → JSON 58 , null : JSON 59 , object : List { mapKey : Text, mapValue : JSON } → JSON 60 , string : Text → JSON 61 } 62 ) → 63 JSON 64 ) 65 ) → 66 ∀(JSON : Type) → 67 ∀ ( json 68 : { array : List JSON → JSON 69 , bool : Bool → JSON 70 , double : Double → JSON 71 , integer : Integer → JSON 72 , null : JSON 73 , object : List { mapKey : Text, mapValue : JSON } → JSON 74 , string : Text → JSON 75 } 76 ) → 77 JSON 78 , bool : 79 ∀(x : Bool) → 80 ∀(JSON : Type) → 81 ∀ ( json 82 : { array : List JSON → JSON 83 , bool : Bool → JSON 84 , double : Double → JSON 85 , integer : Integer → JSON 86 , null : JSON 87 , object : List { mapKey : Text, mapValue : JSON } → JSON 88 , string : Text → JSON 89 } 90 ) → 91 JSON 92 , double : 93 ∀(x : Double) → 94 ∀(JSON : Type) → 95 ∀ ( json 96 : { array : List JSON → JSON 97 , bool : Bool → JSON 98 , double : Double → JSON 99 , integer : Integer → JSON 100 , null : JSON 101 , object : List { mapKey : Text, mapValue : JSON } → JSON 102 , string : Text → JSON 103 } 104 ) → 105 JSON 106 , integer : 107 ∀(x : Integer) → 108 ∀(JSON : Type) → 109 ∀ ( json 110 : { array : List JSON → JSON 111 , bool : Bool → JSON 112 , double : Double → JSON 113 , integer : Integer → JSON 114 , null : JSON 115 , object : List { mapKey : Text, mapValue : JSON } → JSON 116 , string : Text → JSON 117 } 118 ) → 119 JSON 120 , keyText : 121 ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text } 122 , keyValue : 123 ∀(v : Type) → 124 ∀(key : Text) → 125 ∀(value : v) → 126 { mapKey : Text, mapValue : v } 127 , natural : 128 ∀(x : Natural) → 129 ∀(JSON : Type) → 130 ∀ ( json 131 : { array : List JSON → JSON 132 , bool : Bool → JSON 133 , double : Double → JSON 134 , integer : Integer → JSON 135 , null : JSON 136 , object : List { mapKey : Text, mapValue : JSON } → JSON 137 , string : Text → JSON 138 } 139 ) → 140 JSON 141 , null : 142 ∀(JSON : Type) → 143 ∀ ( json 144 : { array : List JSON → JSON 145 , bool : Bool → JSON 146 , double : Double → JSON 147 , integer : Integer → JSON 148 , null : JSON 149 , object : List { mapKey : Text, mapValue : JSON } → JSON 150 , string : Text → JSON 151 } 152 ) → 153 JSON 154 , number : 155 ∀(x : Double) → 156 ∀(JSON : Type) → 157 ∀ ( json 158 : { array : List JSON → JSON 159 , bool : Bool → JSON 160 , double : Double → JSON 161 , integer : Integer → JSON 162 , null : JSON 163 , object : List { mapKey : Text, mapValue : JSON } → JSON 164 , string : Text → JSON 165 } 166 ) → 167 JSON 168 , object : 169 ∀ ( x 170 : List 171 { mapKey : Text 172 , mapValue : 173 ∀(JSON : Type) → 174 ∀ ( json 175 : { array : List JSON → JSON 176 , bool : Bool → JSON 177 , double : Double → JSON 178 , integer : Integer → JSON 179 , null : JSON 180 , object : List { mapKey : Text, mapValue : JSON } → JSON 181 , string : Text → JSON 182 } 183 ) → 184 JSON 185 } 186 ) → 187 ∀(JSON : Type) → 188 ∀ ( json 189 : { array : List JSON → JSON 190 , bool : Bool → JSON 191 , double : Double → JSON 192 , integer : Integer → JSON 193 , null : JSON 194 , object : List { mapKey : Text, mapValue : JSON } → JSON 195 , string : Text → JSON 196 } 197 ) → 198 JSON 199 , omitNullFields : 200 ∀ ( old 201 : ∀(JSON : Type) → 202 ∀ ( json 203 : { array : List JSON → JSON 204 , bool : Bool → JSON 205 , double : Double → JSON 206 , integer : Integer → JSON 207 , null : JSON 208 , object : List { mapKey : Text, mapValue : JSON } → JSON 209 , string : Text → JSON 210 } 211 ) → 212 JSON 213 ) → 214 ∀(JSON : Type) → 215 ∀ ( json 216 : { array : List JSON → JSON 217 , bool : Bool → JSON 218 , double : Double → JSON 219 , integer : Integer → JSON 220 , null : JSON 221 , object : List { mapKey : Text, mapValue : JSON } → JSON 222 , string : Text → JSON 223 } 224 ) → 225 JSON 226 , render : 227 ∀ ( json 228 : ∀(JSON : Type) → 229 ∀ ( json 230 : { array : List JSON → JSON 231 , bool : Bool → JSON 232 , double : Double → JSON 233 , integer : Integer → JSON 234 , null : JSON 235 , object : List { mapKey : Text, mapValue : JSON } → JSON 236 , string : Text → JSON 237 } 238 ) → 239 JSON 240 ) → 241 Text 242 , renderCompact : 243 ∀ ( j 244 : ∀(JSON : Type) → 245 ∀ ( json 246 : { array : List JSON → JSON 247 , bool : Bool → JSON 248 , double : Double → JSON 249 , integer : Integer → JSON 250 , null : JSON 251 , object : List { mapKey : Text, mapValue : JSON } → JSON 252 , string : Text → JSON 253 } 254 ) → 255 JSON 256 ) → 257 Text 258 , renderInteger : ∀(integer : Integer) → Text 259 , renderYAML : 260 ∀ ( json 261 : ∀(JSON : Type) → 262 ∀ ( json 263 : { array : List JSON → JSON 264 , bool : Bool → JSON 265 , double : Double → JSON 266 , integer : Integer → JSON 267 , null : JSON 268 , object : List { mapKey : Text, mapValue : JSON } → JSON 269 , string : Text → JSON 270 } 271 ) → 272 JSON 273 ) → 274 Text 275 , string : 276 ∀(x : Text) → 277 ∀(JSON : Type) → 278 ∀ ( json 279 : { array : List JSON → JSON 280 , bool : Bool → JSON 281 , double : Double → JSON 282 , integer : Integer → JSON 283 , null : JSON 284 , object : List { mapKey : Text, mapValue : JSON } → JSON 285 , string : Text → JSON 286 } 287 ) → 288 JSON 289 , tagInline : 290 ∀(tagFieldName : Text) → 291 ∀(a : Type) → 292 ∀(contents : a) → 293 { contents : a, field : Text, nesting : < Inline | Nested : Text > } 294 , tagNested : 295 ∀(contentsFieldName : Text) → 296 ∀(tagFieldName : Text) → 297 ∀(a : Type) → 298 ∀(contents : a) → 299 { contents : a, field : Text, nesting : < Inline | Nested : Text > } 300 } 301, List : 302 { all : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool 303 , any : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool 304 , build : 305 ∀(a : Type) → 306 (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) → 307 List a 308 , concat : ∀(a : Type) → ∀(xss : List (List a)) → List a 309 , concatMap : 310 ∀(a : Type) → ∀(b : Type) → ∀(f : a → List b) → ∀(xs : List a) → List b 311 , default : ∀(a : Type) → ∀(o : Optional (List a)) → List a 312 , drop : ∀(n : Natural) → ∀(a : Type) → ∀(xs : List a) → List a 313 , empty : ∀(a : Type) → List a 314 , filter : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → List a 315 , fold : 316 ∀(a : Type) → 317 List a → 318 ∀(list : Type) → 319 ∀(cons : a → list → list) → 320 ∀(nil : list) → 321 list 322 , generate : ∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a 323 , head : ∀(a : Type) → List a → Optional a 324 , index : ∀(n : Natural) → ∀(a : Type) → ∀(xs : List a) → Optional a 325 , indexed : ∀(a : Type) → List a → List { index : Natural, value : a } 326 , iterate : ∀(n : Natural) → ∀(a : Type) → ∀(f : a → a) → ∀(x : a) → List a 327 , last : ∀(a : Type) → List a → Optional a 328 , length : ∀(a : Type) → List a → Natural 329 , map : ∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(xs : List a) → List b 330 , null : ∀(a : Type) → ∀(xs : List a) → Bool 331 , partition : 332 ∀(a : Type) → 333 ∀(f : a → Bool) → 334 ∀(xs : List a) → 335 { false : List a, true : List a } 336 , replicate : ∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a 337 , reverse : ∀(a : Type) → List a → List a 338 , shifted : 339 ∀(a : Type) → 340 ∀(kvss : List (List { index : Natural, value : a })) → 341 List { index : Natural, value : a } 342 , take : ∀(n : Natural) → ∀(a : Type) → ∀(xs : List a) → List a 343 , unpackOptionals : ∀(a : Type) → ∀(xs : List (Optional a)) → List a 344 , unzip : 345 ∀(a : Type) → 346 ∀(b : Type) → 347 ∀(xs : List { _1 : a, _2 : b }) → 348 { _1 : List a, _2 : List b } 349 , zip : 350 ∀(a : Type) → 351 ∀(xs : List a) → 352 ∀(b : Type) → 353 ∀(ys : List b) → 354 List { _1 : a, _2 : b } 355 } 356, Location : { Type : Type } 357, Map : 358 { Entry : ∀(k : Type) → ∀(v : Type) → Type 359 , Type : ∀(k : Type) → ∀(v : Type) → Type 360 , empty : ∀(k : Type) → ∀(v : Type) → List { mapKey : k, mapValue : v } 361 , keyText : 362 ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text } 363 , keyValue : 364 ∀(v : Type) → 365 ∀(key : Text) → 366 ∀(value : v) → 367 { mapKey : Text, mapValue : v } 368 , keys : 369 ∀(k : Type) → 370 ∀(v : Type) → 371 ∀(xs : List { mapKey : k, mapValue : v }) → 372 List k 373 , map : 374 ∀(k : Type) → 375 ∀(a : Type) → 376 ∀(b : Type) → 377 ∀(f : a → b) → 378 ∀(m : List { mapKey : k, mapValue : a }) → 379 List { mapKey : k, mapValue : b } 380 , unpackOptionals : 381 ∀(k : Type) → 382 ∀(v : Type) → 383 ∀(xs : List { mapKey : k, mapValue : Optional v }) → 384 List { mapKey : k, mapValue : v } 385 , values : 386 ∀(k : Type) → 387 ∀(v : Type) → 388 ∀(xs : List { mapKey : k, mapValue : v }) → 389 List v 390 } 391, Monoid : ∀(m : Type) → Type 392, Natural : 393 { build : 394 ( ∀(natural : Type) → 395 ∀(succ : natural → natural) → 396 ∀(zero : natural) → 397 natural 398 ) → 399 Natural 400 , enumerate : ∀(n : Natural) → List Natural 401 , equal : ∀(a : Natural) → ∀(b : Natural) → Bool 402 , even : Natural → Bool 403 , fold : 404 Natural → 405 ∀(natural : Type) → 406 ∀(succ : natural → natural) → 407 ∀(zero : natural) → 408 natural 409 , greaterThan : ∀(x : Natural) → ∀(y : Natural) → Bool 410 , greaterThanEqual : ∀(x : Natural) → ∀(y : Natural) → Bool 411 , isZero : Natural → Bool 412 , lessThan : ∀(x : Natural) → ∀(y : Natural) → Bool 413 , lessThanEqual : ∀(x : Natural) → ∀(y : Natural) → Bool 414 , listMax : ∀(xs : List Natural) → Optional Natural 415 , listMin : ∀(xs : List Natural) → Optional Natural 416 , max : ∀(a : Natural) → ∀(b : Natural) → Natural 417 , min : ∀(a : Natural) → ∀(b : Natural) → Natural 418 , odd : Natural → Bool 419 , product : ∀(xs : List Natural) → Natural 420 , show : Natural → Text 421 , sort : ∀(xs : List Natural) → List Natural 422 , subtract : Natural → Natural → Natural 423 , sum : ∀(xs : List Natural) → Natural 424 , toDouble : ∀(n : Natural) → Double 425 , toInteger : Natural → Integer 426 } 427, Operator : 428 { `!=` : ∀(m : Bool) → ∀(n : Bool) → Bool 429 , `#` : ∀(type : Type) → ∀(m : List type) → ∀(n : List type) → List type 430 , `&&` : ∀(m : Bool) → ∀(n : Bool) → Bool 431 , `*` : ∀(m : Natural) → ∀(n : Natural) → Natural 432 , `+` : ∀(m : Natural) → ∀(n : Natural) → Natural 433 , `++` : ∀(m : Text) → ∀(n : Text) → Text 434 , `==` : ∀(m : Bool) → ∀(n : Bool) → Bool 435 , `||` : ∀(m : Bool) → ∀(n : Bool) → Bool 436 } 437, Optional : 438 { all : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool 439 , any : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool 440 , build : 441 ∀(a : Type) → 442 ∀ ( build 443 : ∀(optional : Type) → 444 ∀(some : a → optional) → 445 ∀(none : optional) → 446 optional 447 ) → 448 Optional a 449 , concat : ∀(a : Type) → ∀(x : Optional (Optional a)) → Optional a 450 , concatMap : 451 ∀(a : Type) → 452 ∀(b : Type) → 453 ∀(f : a → Optional b) → 454 ∀(o : Optional a) → 455 Optional b 456 , default : ∀(a : Type) → ∀(default : a) → ∀(o : Optional a) → a 457 , filter : ∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Optional a 458 , fold : 459 ∀(a : Type) → 460 ∀(o : Optional a) → 461 ∀(optional : Type) → 462 ∀(some : a → optional) → 463 ∀(none : optional) → 464 optional 465 , head : ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a 466 , last : ∀(a : Type) → ∀(xs : List (Optional a)) → Optional a 467 , length : ∀(a : Type) → ∀(xs : Optional a) → Natural 468 , map : 469 ∀(a : Type) → 470 ∀(b : Type) → 471 ∀(f : a → b) → 472 ∀(o : Optional a) → 473 Optional b 474 , null : ∀(a : Type) → ∀(xs : Optional a) → Bool 475 , toList : ∀(a : Type) → ∀(o : Optional a) → List a 476 , unzip : 477 ∀(a : Type) → 478 ∀(b : Type) → 479 ∀(xs : Optional { _1 : a, _2 : b }) → 480 { _1 : Optional a, _2 : Optional b } 481 } 482, Text : 483 { concat : ∀(xs : List Text) → Text 484 , concatMap : ∀(a : Type) → ∀(f : a → Text) → ∀(xs : List a) → Text 485 , concatMapSep : 486 ∀(separator : Text) → 487 ∀(a : Type) → 488 ∀(f : a → Text) → 489 ∀(elements : List a) → 490 Text 491 , concatSep : ∀(separator : Text) → ∀(elements : List Text) → Text 492 , default : ∀(o : Optional Text) → Text 493 , defaultMap : ∀(a : Type) → ∀(f : a → Text) → ∀(o : Optional a) → Text 494 , replace : 495 ∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text 496 , replicate : ∀(num : Natural) → ∀(text : Text) → Text 497 , show : Text → Text 498 , spaces : ∀(a : Natural) → Text 499 } 500, XML : 501 { Type : Type 502 , attribute : 503 ∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text } 504 , element : 505 ∀ ( elem 506 : { attributes : List { mapKey : Text, mapValue : Text } 507 , content : 508 List 509 ( ∀(XML : Type) → 510 ∀ ( xml 511 : { element : 512 { attributes : 513 List { mapKey : Text, mapValue : Text } 514 , content : List XML 515 , name : Text 516 } → 517 XML 518 , text : Text → XML 519 } 520 ) → 521 XML 522 ) 523 , name : Text 524 } 525 ) → 526 ∀(XML : Type) → 527 ∀ ( xml 528 : { element : 529 { attributes : List { mapKey : Text, mapValue : Text } 530 , content : List XML 531 , name : Text 532 } → 533 XML 534 , text : Text → XML 535 } 536 ) → 537 XML 538 , emptyAttributes : List { mapKey : Text, mapValue : Text } 539 , leaf : 540 ∀ ( elem 541 : { attributes : List { mapKey : Text, mapValue : Text } 542 , name : Text 543 } 544 ) → 545 ∀(XML : Type) → 546 ∀ ( xml 547 : { element : 548 { attributes : List { mapKey : Text, mapValue : Text } 549 , content : List XML 550 , name : Text 551 } → 552 XML 553 , text : Text → XML 554 } 555 ) → 556 XML 557 , render : 558 ∀ ( x 559 : ∀(XML : Type) → 560 ∀ ( xml 561 : { element : 562 { attributes : List { mapKey : Text, mapValue : Text } 563 , content : List XML 564 , name : Text 565 } → 566 XML 567 , text : Text → XML 568 } 569 ) → 570 XML 571 ) → 572 Text 573 , text : 574 ∀(d : Text) → 575 ∀(XML : Type) → 576 ∀ ( xml 577 : { element : 578 { attributes : List { mapKey : Text, mapValue : Text } 579 , content : List XML 580 , name : Text 581 } → 582 XML 583 , text : Text → XML 584 } 585 ) → 586 XML 587 } 588} 589