@@ -474,12 +474,12 @@ import Dhall
474
474
--
475
475
-- __Exercise:__ There is a @not@ function hosted online here:
476
476
--
477
- -- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not>
477
+ -- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not>
478
478
--
479
479
-- Visit that link and read the documentation. Then try to guess what this
480
480
-- code returns:
481
481
--
482
- -- > >>> input auto "https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
482
+ -- > >>> input auto "https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
483
483
-- > ???
484
484
--
485
485
-- Run the code to test your guess
@@ -966,7 +966,7 @@ import Dhall
966
966
-- You can also use @let@ expressions to rename imports, like this:
967
967
--
968
968
-- > $ dhall
969
- -- > let not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not
969
+ -- > let not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not
970
970
-- > in not True
971
971
-- > <Ctrl-D>
972
972
-- > Bool
@@ -1324,7 +1324,7 @@ import Dhall
1324
1324
-- complex example:
1325
1325
--
1326
1326
-- > $ dhall
1327
- -- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/map
1327
+ -- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/map
1328
1328
-- > in λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3]
1329
1329
-- > <Ctrl-D>
1330
1330
-- > ∀(f : Integer → Integer) → List Integer
@@ -1348,11 +1348,11 @@ import Dhall
1348
1348
-- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can
1349
1349
-- find here:
1350
1350
--
1351
- -- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/replicate>
1351
+ -- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/replicate>
1352
1352
--
1353
1353
-- Test what the following Dhall expression normalizes to:
1354
1354
--
1355
- -- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/replicate
1355
+ -- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/replicate
1356
1356
-- > in replicate +10
1357
1357
--
1358
1358
-- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by
@@ -1604,11 +1604,11 @@ import Dhall
1604
1604
-- normalizing them:
1605
1605
--
1606
1606
-- > $ dhall-format
1607
- -- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/replicate
1607
+ -- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/replicate
1608
1608
-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
1609
1609
-- > <Ctrl-D>
1610
1610
-- > let replicate =
1611
- -- > https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/replicate
1611
+ -- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/replicate
1612
1612
-- >
1613
1613
-- > in replicate
1614
1614
-- > +5
@@ -1619,7 +1619,7 @@ import Dhall
1619
1619
-- @--pretty@ flag of the @dhall@ executable:
1620
1620
--
1621
1621
-- > $ dhall --pretty
1622
- -- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/replicate
1622
+ -- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/replicate
1623
1623
-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
1624
1624
-- > <Ctrl-D>
1625
1625
-- > List (List (List Integer))
@@ -2283,7 +2283,7 @@ import Dhall
2283
2283
--
2284
2284
-- Rules:
2285
2285
--
2286
- -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concat
2286
+ -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concat
2287
2287
-- >
2288
2288
-- > List/fold a (Prelude/List/concat a xss) b c
2289
2289
-- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)
@@ -2352,10 +2352,10 @@ import Dhall
2352
2352
--
2353
2353
-- Rules:
2354
2354
--
2355
- -- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Optional/head
2356
- -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concat
2357
- -- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concatMap
2358
- -- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/map
2355
+ -- > let Prelude/Optional/head = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Optional/head
2356
+ -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concat
2357
+ -- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concatMap
2358
+ -- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/map
2359
2359
-- >
2360
2360
-- > List/head a (Prelude/List/concat a xss) =
2361
2361
-- > Prelude/Optional/head a (Prelude/List/map (List a) (Optional a) (List/head a) xss)
@@ -2383,10 +2383,10 @@ import Dhall
2383
2383
--
2384
2384
-- Rules:
2385
2385
--
2386
- -- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Optional/last
2387
- -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concat
2388
- -- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concatMap
2389
- -- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/map
2386
+ -- > let Prelude/Optional/last = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Optional/last
2387
+ -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concat
2388
+ -- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concatMap
2389
+ -- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/map
2390
2390
-- >
2391
2391
-- > List/last a (Prelude/List/concat a xss) =
2392
2392
-- > Prelude/Optional/last a (Prelude/List/map (List a) (Optional a) (List/last a) xss)
@@ -2414,9 +2414,9 @@ import Dhall
2414
2414
--
2415
2415
-- Rules:
2416
2416
--
2417
- -- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/shifted
2418
- -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concat
2419
- -- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/map
2417
+ -- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/shifted
2418
+ -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concat
2419
+ -- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/map
2420
2420
-- >
2421
2421
-- > List/indexed a (Prelude/List/concat a xss) =
2422
2422
-- > Prelude/List/shifted a (Prelude/List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)
@@ -2439,9 +2439,9 @@ import Dhall
2439
2439
--
2440
2440
-- Rules:
2441
2441
--
2442
- -- > let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/map
2443
- -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concat
2444
- -- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/List/concatMap
2442
+ -- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/map
2443
+ -- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concat
2444
+ -- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/List/concatMap
2445
2445
-- >
2446
2446
-- > List/reverse a (Prelude/List/concat a xss)
2447
2447
-- > = Prelude/List/concat a (List/reverse (List a) (Prelude/List/map (List a) (List a) (List/reverse a) xss))
@@ -2499,7 +2499,7 @@ import Dhall
2499
2499
--
2500
2500
-- ... which currenty redirects to:
2501
2501
--
2502
- -- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude>
2502
+ -- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude>
2503
2503
--
2504
2504
-- There is nothing \"official\" or \"standard\" about this Prelude other than
2505
2505
-- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a
@@ -2510,12 +2510,12 @@ import Dhall
2510
2510
-- subdirectories. For example, the @Bool@ subdirectory has a @not@ file
2511
2511
-- located here:
2512
2512
--
2513
- -- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not>
2513
+ -- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not>
2514
2514
--
2515
2515
-- The @not@ function is just a UTF8-encoded text file hosted online with the
2516
2516
-- following contents
2517
2517
--
2518
- -- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not
2518
+ -- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not
2519
2519
-- > {-
2520
2520
-- > Flip the value of a `Bool`
2521
2521
-- >
@@ -2548,7 +2548,7 @@ import Dhall
2548
2548
-- You can use this @not@ function either directly:
2549
2549
--
2550
2550
-- > $ dhall
2551
- -- > https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not True
2551
+ -- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not True
2552
2552
-- > <Ctrl-D>
2553
2553
-- > Bool
2554
2554
-- >
@@ -2557,7 +2557,7 @@ import Dhall
2557
2557
-- ... or assign the URL to a shorter name:
2558
2558
--
2559
2559
-- > $ dhall
2560
- -- > let Bool/not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Bool/not
2560
+ -- > let Bool/not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Bool/not
2561
2561
-- > in Bool/not True
2562
2562
-- > <Ctrl-D>
2563
2563
-- > Bool
@@ -2568,7 +2568,7 @@ import Dhall
2568
2568
-- consistency and documentation, such as @Prelude\/Natural\/even@, which
2569
2569
-- re-exports the built-in @Natural/even@ function:
2570
2570
--
2571
- -- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/Natural/even
2571
+ -- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/Natural/even
2572
2572
-- > {-
2573
2573
-- > Returns `True` if a number if even and returns `False` otherwise
2574
2574
-- >
@@ -2589,7 +2589,7 @@ import Dhall
2589
2589
-- using local relative paths instead of URLs. For example, you can use @wget@,
2590
2590
-- like this:
2591
2591
--
2592
- -- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/
2592
+ -- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/
2593
2593
-- > $ tree Prelude
2594
2594
-- > Prelude
2595
2595
-- > ├── Bool
@@ -2653,12 +2653,12 @@ import Dhall
2653
2653
-- locally like this:
2654
2654
--
2655
2655
-- > $ ipfs mount
2656
- -- > $ cd /ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude
2656
+ -- > $ cd /ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude
2657
2657
--
2658
2658
-- Browse the Prelude online to learn more by seeing what functions are
2659
2659
-- available and reading their inline documentation:
2660
2660
--
2661
- -- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude>
2661
+ -- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude>
2662
2662
--
2663
2663
-- __Exercise__: Try to use a new Prelude function that has not been covered
2664
2664
-- previously in this tutorial
@@ -2667,7 +2667,7 @@ import Dhall
2667
2667
-- convenience:
2668
2668
--
2669
2669
-- > $ dhall
2670
- -- > let Prelude = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/package.dhall
2670
+ -- > let Prelude = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/package.dhall
2671
2671
-- >
2672
2672
-- > in λ(x : Text)
2673
2673
-- > → Prelude.`List`.length Text (Prelude.`List`.replicate +10 Text x)
@@ -2682,7 +2682,7 @@ import Dhall
2682
2682
--
2683
2683
-- __Exercise__: Browse the Prelude by running:
2684
2684
--
2685
- -- > $ dhall --pretty <<< 'https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx /Prelude/package.dhall'
2685
+ -- > $ dhall --pretty <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB /Prelude/package.dhall'
2686
2686
2687
2687
-- $conclusion
2688
2688
--
0 commit comments