Update Prelude hash
This commit is contained in:
Gabriel Gonzalez
parent
2d7fe03ae0
commit
0873c6efc6
|
|
@ -459,12 +459,12 @@ import Dhall
|
|||
--
|
||||
-- __Exercise:__ There is a @not@ function hosted online here:
|
||||
--
|
||||
-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not>
|
||||
-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not>
|
||||
--
|
||||
-- Visit that link and read the documentation. Then try to guess what this
|
||||
-- code returns:
|
||||
--
|
||||
-- > >>> input auto "https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
|
||||
-- > >>> input auto "https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool
|
||||
-- > ???
|
||||
--
|
||||
-- Run the code to test your guess
|
||||
|
|
@ -928,7 +928,7 @@ import Dhall
|
|||
-- You can also use @let@ expressions to rename imports, like this:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > let not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not
|
||||
-- > let not = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not
|
||||
-- > in not True
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
|
|
@ -1214,7 +1214,7 @@ import Dhall
|
|||
-- complex example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
|
||||
-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map
|
||||
-- > in λ(f : Integer → Integer) → List/map Integer Integer f [1, 2, 3]
|
||||
-- > <Ctrl-D>
|
||||
-- > ∀(f : Integer → Integer) → List Integer
|
||||
|
|
@ -1238,11 +1238,11 @@ import Dhall
|
|||
-- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can
|
||||
-- find here:
|
||||
--
|
||||
-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate>
|
||||
-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/replicate>
|
||||
--
|
||||
-- Test what the following Dhall expression normalizes to:
|
||||
--
|
||||
-- > let replicate = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate
|
||||
-- > let replicate = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/replicate
|
||||
-- > in replicate +10
|
||||
--
|
||||
-- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by
|
||||
|
|
@ -1836,7 +1836,7 @@ import Dhall
|
|||
--
|
||||
-- Rules:
|
||||
--
|
||||
-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat
|
||||
-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat
|
||||
-- >
|
||||
-- > List/fold a (List/concat a xss) b c
|
||||
-- > = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)
|
||||
|
|
@ -1905,10 +1905,10 @@ import Dhall
|
|||
--
|
||||
-- Rules:
|
||||
--
|
||||
-- > let Optional/head = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/head
|
||||
-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat
|
||||
-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap
|
||||
-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
|
||||
-- > let Optional/head = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Optional/head
|
||||
-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat
|
||||
-- > let List/concatMap = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concatMap
|
||||
-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map
|
||||
-- >
|
||||
-- > List/head a (List/concat a xss) =
|
||||
-- > Optional/head a (List/map (List a) (Optional a) (List/head a) xss)
|
||||
|
|
@ -1936,10 +1936,10 @@ import Dhall
|
|||
--
|
||||
-- Rules:
|
||||
--
|
||||
-- > let Optional/last = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/last
|
||||
-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat
|
||||
-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap
|
||||
-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
|
||||
-- > let Optional/last = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Optional/last
|
||||
-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat
|
||||
-- > let List/concatMap = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concatMap
|
||||
-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map
|
||||
-- >
|
||||
-- > List/last a (List/concat a xss) =
|
||||
-- > Optional/last a (List/map (List a) (Optional a) (List/last a) xss)
|
||||
|
|
@ -1967,9 +1967,9 @@ import Dhall
|
|||
--
|
||||
-- Rules:
|
||||
--
|
||||
-- > let List/shifted = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/shifted
|
||||
-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat
|
||||
-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
|
||||
-- > let List/shifted = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/shifted
|
||||
-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat
|
||||
-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map
|
||||
-- >
|
||||
-- > List/indexed a (List/concat a xss) =
|
||||
-- > List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)
|
||||
|
|
@ -1992,9 +1992,9 @@ import Dhall
|
|||
--
|
||||
-- Rules:
|
||||
--
|
||||
-- > let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map
|
||||
-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat
|
||||
-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap
|
||||
-- > let List/map = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/map
|
||||
-- > let List/concat = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concat
|
||||
-- > let List/concatMap = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/List/concatMap
|
||||
-- >
|
||||
-- > List/reverse a (List/concat a xss)
|
||||
-- > = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss))
|
||||
|
|
@ -2048,7 +2048,7 @@ import Dhall
|
|||
--
|
||||
-- There is also a Prelude available at:
|
||||
--
|
||||
-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude>
|
||||
-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude>
|
||||
--
|
||||
-- There is nothing \"official\" or \"standard\" about this Prelude other than
|
||||
-- the fact that it is mentioned in this tutorial. The \"Prelude\" is just a
|
||||
|
|
@ -2059,12 +2059,12 @@ import Dhall
|
|||
-- subdirectories. For example, the @Bool@ subdirectory has a @not@ file
|
||||
-- located here:
|
||||
--
|
||||
-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not>
|
||||
-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not>
|
||||
--
|
||||
-- The @not@ function is just a UTF8-encoded text file hosted online with the
|
||||
-- following contents
|
||||
--
|
||||
-- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not
|
||||
-- > $ curl https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not
|
||||
-- > {-
|
||||
-- > Flip the value of a `Bool`
|
||||
-- >
|
||||
|
|
@ -2097,7 +2097,7 @@ import Dhall
|
|||
-- You can use this @not@ function either directly:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not True
|
||||
-- > https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not True
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
-- >
|
||||
|
|
@ -2106,7 +2106,7 @@ import Dhall
|
|||
-- ... or assign the URL to a shorter name:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > let Bool/not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not
|
||||
-- > let Bool/not = https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Bool/not
|
||||
-- > in Bool/not True
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
|
|
@ -2117,7 +2117,7 @@ import Dhall
|
|||
-- consistency and documentation, such as @Prelude\/Natural\/even@, which
|
||||
-- re-exports the built-in @Natural/even@ function:
|
||||
--
|
||||
-- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Natural/even
|
||||
-- > $ curl https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/Natural/even
|
||||
-- > {-
|
||||
-- > Returns `True` if a number if even and returns `False` otherwise
|
||||
-- >
|
||||
|
|
@ -2138,7 +2138,7 @@ import Dhall
|
|||
-- using local relative paths instead of URLs. For example, you can use @wget@,
|
||||
-- like this:
|
||||
--
|
||||
-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/
|
||||
-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude/
|
||||
-- > $ tree Prelude
|
||||
-- > Prelude
|
||||
-- > ├── Bool
|
||||
|
|
@ -2202,12 +2202,12 @@ import Dhall
|
|||
-- locally like this:
|
||||
--
|
||||
-- > $ ipfs mount
|
||||
-- > $ cd /ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude
|
||||
-- > $ cd /ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude
|
||||
--
|
||||
-- Browse the Prelude online to learn more by seeing what functions are
|
||||
-- available and reading their inline documentation:
|
||||
--
|
||||
-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude>
|
||||
-- <https://ipfs.io/ipfs/QmRHdo2Jg59EZUT8Toq7MCZFN6e7wNbBtvaF7HCTrDFPxG/Prelude>
|
||||
--
|
||||
-- __Exercise__: Try to use a new Prelude function that has not been covered
|
||||
-- previously in this tutorial
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user