diff --git a/Prelude/Bool/and b/Prelude/Bool/and index 3d8633876..1bc679fde 100644 --- a/Prelude/Bool/and +++ b/Prelude/Bool/and @@ -10,9 +10,9 @@ Examples: ./and ([] : List Bool) = True ``` -} - let and - : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True +let and + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True in and diff --git a/Prelude/Bool/build b/Prelude/Bool/build index 85ca48406..401c78626 100644 --- a/Prelude/Bool/build +++ b/Prelude/Bool/build @@ -9,9 +9,9 @@ Examples: ./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) = False ``` -} - let build - : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool - = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) - → f Bool True False +let build + : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool + = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) + → f Bool True False in build diff --git a/Prelude/Bool/even b/Prelude/Bool/even index b4eb5e953..8e65dcfec 100644 --- a/Prelude/Bool/even +++ b/Prelude/Bool/even @@ -14,9 +14,9 @@ Examples: ./even ([] : List Bool) = True ``` -} - let even - : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True +let even + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True in even diff --git a/Prelude/Bool/fold b/Prelude/Bool/fold index e8e2b5610..15e04021b 100644 --- a/Prelude/Bool/fold +++ b/Prelude/Bool/fold @@ -9,12 +9,12 @@ Examples: ./fold False Natural 0 1 = 1 ``` -} - let fold - : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool - = λ(b : Bool) - → λ(bool : Type) - → λ(true : bool) - → λ(false : bool) - → if b then true else false +let fold + : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool + = λ(b : Bool) + → λ(bool : Type) + → λ(true : bool) + → λ(false : bool) + → if b then true else false in fold diff --git a/Prelude/Bool/odd b/Prelude/Bool/odd index 8ad485a7d..d5c4eee25 100644 --- a/Prelude/Bool/odd +++ b/Prelude/Bool/odd @@ -14,9 +14,9 @@ Examples: ./odd ([] : List Bool) = False ``` -} - let odd - : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False +let odd + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False in odd diff --git a/Prelude/Bool/or b/Prelude/Bool/or index e3ae1e2d1..4867b01cb 100644 --- a/Prelude/Bool/or +++ b/Prelude/Bool/or @@ -10,9 +10,9 @@ Examples: ./or ([] : List Bool) = False ``` -} - let or - : List Bool → Bool - = λ(xs : List Bool) - → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False +let or + : List Bool → Bool + = λ(xs : List Bool) + → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False in or diff --git a/Prelude/Bool/package.dhall b/Prelude/Bool/package.dhall index 3902ffa93..35f1b7901 100644 --- a/Prelude/Bool/package.dhall +++ b/Prelude/Bool/package.dhall @@ -1,25 +1,25 @@ { and = - ./and sha256:0b2114fa33cd76652e4360f012bc082718944fe4c5b28c975483178f8d9b0a6d + ./and sha256:0b2114fa33cd76652e4360f012bc082718944fe4c5b28c975483178f8d9b0a6d ? ./and , build = - ./build sha256:add7cb9acacac705410088d876a7e4488e046a7aded304f06c51accffd7f1b7b + ./build sha256:add7cb9acacac705410088d876a7e4488e046a7aded304f06c51accffd7f1b7b ? ./build , even = - ./even sha256:72a05ee550636a3acb768360fa51ba0db0326763e0cf1ceb737f0f3607fc0fe5 + ./even sha256:72a05ee550636a3acb768360fa51ba0db0326763e0cf1ceb737f0f3607fc0fe5 ? ./even , fold = - ./fold sha256:39f60baf3950268c2e849e91dc6279ee41cd6b81892d54020d4fcd2ce30a96ae + ./fold sha256:39f60baf3950268c2e849e91dc6279ee41cd6b81892d54020d4fcd2ce30a96ae ? ./fold , not = - ./not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4 + ./not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4 ? ./not , odd = - ./odd sha256:6360fca3a745de32bd186cc7b71487a6398cd47d5119064eae491872c41d1999 + ./odd sha256:6360fca3a745de32bd186cc7b71487a6398cd47d5119064eae491872c41d1999 ? ./odd , or = - ./or sha256:5c50738e84e1c4fed8343ebd57608500e1b61ac1f502aa52d6d6edb5c20b99e4 + ./or sha256:5c50738e84e1c4fed8343ebd57608500e1b61ac1f502aa52d6d6edb5c20b99e4 ? ./or , show = - ./show sha256:f85f6d2d921c37a2122cb2e2f8a0170e305b699debd0e6df5ef3370d806b5f61 + ./show sha256:f85f6d2d921c37a2122cb2e2f8a0170e305b699debd0e6df5ef3370d806b5f61 ? ./show } diff --git a/Prelude/Double/package.dhall b/Prelude/Double/package.dhall index 77afbbb24..4922c17a0 100644 --- a/Prelude/Double/package.dhall +++ b/Prelude/Double/package.dhall @@ -1,4 +1,4 @@ { show = - ./show sha256:ae645813cc4d8505a265df4d7564c95482f62bb3e07fc81681959599b6cee04f + ./show sha256:ae645813cc4d8505a265df4d7564c95482f62bb3e07fc81681959599b6cee04f ? ./show } diff --git a/Prelude/Function/compose b/Prelude/Function/compose index bae6a662b..f9f43b622 100644 --- a/Prelude/Function/compose +++ b/Prelude/Function/compose @@ -8,14 +8,14 @@ Examples: = True ``` -} - let compose - : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c - = λ(A : Type) - → λ(B : Type) - → λ(C : Type) - → λ(f : A → B) - → λ(g : B → C) - → λ(x : A) - → g (f x) +let compose + : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c + = λ(A : Type) + → λ(B : Type) + → λ(C : Type) + → λ(f : A → B) + → λ(g : B → C) + → λ(x : A) + → g (f x) in compose diff --git a/Prelude/Function/package.dhall b/Prelude/Function/package.dhall index dc9e00ab5..6d3868eb7 100644 --- a/Prelude/Function/package.dhall +++ b/Prelude/Function/package.dhall @@ -1,4 +1,4 @@ { compose = - ./compose sha256:65ad8bbea530b3d8968785a7cf4a9a7976b67059aa15e3b61fcba600a40ae013 + ./compose sha256:65ad8bbea530b3d8968785a7cf4a9a7976b67059aa15e3b61fcba600a40ae013 ? ./compose } diff --git a/Prelude/Integer/package.dhall b/Prelude/Integer/package.dhall index a55b30f88..5361ea0be 100644 --- a/Prelude/Integer/package.dhall +++ b/Prelude/Integer/package.dhall @@ -1,7 +1,7 @@ { show = - ./show sha256:ecf8b0594cd5181bc45d3b7ea0d44d3ba9ad5dac6ec17bb8968beb65f4b1baa9 + ./show sha256:ecf8b0594cd5181bc45d3b7ea0d44d3ba9ad5dac6ec17bb8968beb65f4b1baa9 ? ./show , toDouble = - ./toDouble sha256:77bc5d635dc4d952f37cc96f2a681d5ac503b4e8b21fc00055b1946adb5beda7 + ./toDouble sha256:77bc5d635dc4d952f37cc96f2a681d5ac503b4e8b21fc00055b1946adb5beda7 ? ./toDouble } diff --git a/Prelude/JSON/Nesting b/Prelude/JSON/Nesting index bf0de5053..30b7b4508 100644 --- a/Prelude/JSON/Nesting +++ b/Prelude/JSON/Nesting @@ -5,17 +5,16 @@ names For example, this Dhall code: ``` - let Example = < Left : { foo : Natural } | Right : { bar : Bool } > +let Example = < Left : { foo : Natural } | Right : { bar : Bool } > -in let example = constructors Example +let Nesting = < Inline : {} | Nested : Text > -in let Nesting = < Inline : {} | Nested : Text > - -in let nesting = constructors Nesting - -in { field = "name" - , nesting = nesting.Inline {=} - , contents = example.Left { foo = 2 } +in { field = + "name" + , nesting = + Nesting.Inline {=} + , contents = + Example.Left { foo = 2 } } ``` diff --git a/Prelude/JSON/Tagged b/Prelude/JSON/Tagged index 9b731d6b4..021b4c744 100644 --- a/Prelude/JSON/Tagged +++ b/Prelude/JSON/Tagged @@ -5,33 +5,31 @@ for preserving alternative names For example, this code: ``` - let map = ../List/map +let map = ../List/map -in let Provisioner = - < shell : - { inline : List Text } - | file : - { source : Text, destination : Text } - > +let Provisioner = + < shell : + { inline : List Text } + | file : + { source : Text, destination : Text } + > -in let provisioner = constructors Provisioner +let Tagged = ./Tagged -in let Tagged = ./Tagged +let Nesting = ./Nesting -in let nesting = constructors ./Nesting - -in let wrap - : Provisioner → Tagged Provisioner - = λ(x : Provisioner) - → { field = "type", nesting = nesting.Nested "params", contents = x } +let wrap + : Provisioner → Tagged Provisioner + = λ(x : Provisioner) + → { field = "type", nesting = Nesting.Nested "params", contents = x } in { provisioners = map Provisioner (Tagged Provisioner) wrap - [ provisioner.shell { inline = [ "echo foo" ] } - , provisioner.file + [ Provisioner.shell { inline = [ "echo foo" ] } + , Provisioner.file { source = "app.tar.gz", destination = "/tmp/app.tar.gz" } ] } @@ -62,8 +60,8 @@ in { provisioners = ``` -} - let Tagged - : Type → Type - = λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a } +let Tagged + : Type → Type + = λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a } in Tagged diff --git a/Prelude/JSON/keyText b/Prelude/JSON/keyText index eabb77daa..3c7ca81f9 100644 --- a/Prelude/JSON/keyText +++ b/Prelude/JSON/keyText @@ -11,7 +11,7 @@ Example: ``` -} - let keyText = - λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value } +let keyText = + λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value } in keyText diff --git a/Prelude/JSON/keyValue b/Prelude/JSON/keyValue index 0e5e36238..655aecd01 100644 --- a/Prelude/JSON/keyValue +++ b/Prelude/JSON/keyValue @@ -11,10 +11,10 @@ Examples: ``` -} - let keyValue = - λ(v : Type) - → λ(key : Text) - → λ(value : v) - → { mapKey = key, mapValue = value } +let keyValue = + λ(v : Type) + → λ(key : Text) + → λ(value : v) + → { mapKey = key, mapValue = value } in keyValue diff --git a/Prelude/JSON/package.dhall b/Prelude/JSON/package.dhall index a32b986d9..e89006fc7 100644 --- a/Prelude/JSON/package.dhall +++ b/Prelude/JSON/package.dhall @@ -1,7 +1,7 @@ { keyText = - ./keyText sha256:f7b6c802ca5764d03d5e9a6e48d9cb167c01392f775d9c2c87b83cdaa60ea0cc + ./keyText sha256:f7b6c802ca5764d03d5e9a6e48d9cb167c01392f775d9c2c87b83cdaa60ea0cc ? ./keyText , keyValue = - ./keyValue sha256:a0a97199d280c4cce72ffcbbf93b7ceda0a569cf4d173ac98e0aaaa78034b98c + ./keyValue sha256:a0a97199d280c4cce72ffcbbf93b7ceda0a569cf4d173ac98e0aaaa78034b98c ? ./keyValue } diff --git a/Prelude/List/all b/Prelude/List/all index f7456d910..a49b926a0 100644 --- a/Prelude/List/all +++ b/Prelude/List/all @@ -10,11 +10,11 @@ Examples: ./all Natural Natural/even ([] : List Natural) = True ``` -} - let all - : ∀(a : Type) → (a → Bool) → List a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : List a) - → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True +let all + : ∀(a : Type) → (a → Bool) → List a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : List a) + → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True in all diff --git a/Prelude/List/any b/Prelude/List/any index 225da845f..9ba6f3bf8 100644 --- a/Prelude/List/any +++ b/Prelude/List/any @@ -10,11 +10,11 @@ Examples: ./any Natural Natural/even ([] : List Natural) = False ``` -} - let any - : ∀(a : Type) → (a → Bool) → List a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : List a) - → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False +let any + : ∀(a : Type) → (a → Bool) → List a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : List a) + → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False in any diff --git a/Prelude/List/build b/Prelude/List/build index c05572e5e..482154491 100644 --- a/Prelude/List/build +++ b/Prelude/List/build @@ -23,10 +23,10 @@ Text = [] : List Text ``` -} - let build - : ∀(a : Type) - → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) - → List a - = List/build +let build + : ∀(a : Type) + → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) + → List a + = List/build in build diff --git a/Prelude/List/concat b/Prelude/List/concat index 2f7291b76..604e7b5a1 100644 --- a/Prelude/List/concat +++ b/Prelude/List/concat @@ -22,21 +22,21 @@ Examples: ./concat Natural ([] : List (List Natural)) = [] : List Natural ``` -} - let concat - : ∀(a : Type) → List (List a) → List a - = λ(a : Type) - → λ(xss : List (List a)) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → λ(nil : list) - → List/fold - (List a) - xss - list - (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys) - nil - ) +let concat + : ∀(a : Type) → List (List a) → List a + = λ(a : Type) + → λ(xss : List (List a)) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → λ(nil : list) + → List/fold + (List a) + xss + list + (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys) + nil + ) in concat diff --git a/Prelude/List/concatMap b/Prelude/List/concatMap index f54f491ea..2cde97ea9 100644 --- a/Prelude/List/concatMap +++ b/Prelude/List/concatMap @@ -12,17 +12,17 @@ Examples: = [] : List Natural ``` -} - let concatMap - : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b - = λ(a : Type) - → λ(b : Type) - → λ(f : a → List b) - → λ(xs : List a) - → List/build - b - ( λ(list : Type) - → λ(cons : b → list → list) - → List/fold a xs list (λ(x : a) → List/fold b (f x) list cons) - ) +let concatMap + : ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b + = λ(a : Type) + → λ(b : Type) + → λ(f : a → List b) + → λ(xs : List a) + → List/build + b + ( λ(list : Type) + → λ(cons : b → list → list) + → List/fold a xs list (λ(x : a) → List/fold b (f x) list cons) + ) in concatMap diff --git a/Prelude/List/filter b/Prelude/List/filter index 3edeb5872..d0a6b6a92 100644 --- a/Prelude/List/filter +++ b/Prelude/List/filter @@ -11,20 +11,20 @@ Examples: = [ 3, 5 ] ``` -} - let filter - : ∀(a : Type) → (a → Bool) → List a → List a - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : List a) - → List/build +let filter + : ∀(a : Type) → (a → Bool) → List a → List a + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : List a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - a - xs - list - (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs) - ) + xs + list + (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs) + ) in filter diff --git a/Prelude/List/fold b/Prelude/List/fold index 5307ea7a9..7499b2f17 100644 --- a/Prelude/List/fold +++ b/Prelude/List/fold @@ -34,13 +34,13 @@ Examples: → cons 2 (cons 3 (cons 5 nil)) ``` -} - let fold - : ∀(a : Type) - → List a - → ∀(list : Type) - → ∀(cons : a → list → list) - → ∀(nil : list) - → list - = List/fold +let fold + : ∀(a : Type) + → List a + → ∀(list : Type) + → ∀(cons : a → list → list) + → ∀(nil : list) + → list + = List/fold in fold diff --git a/Prelude/List/generate b/Prelude/List/generate index 3397fa8b2..cabe81426 100644 --- a/Prelude/List/generate +++ b/Prelude/List/generate @@ -10,29 +10,29 @@ Examples: ./generate 0 Bool Natural/even = [] : List Bool ``` -} - let generate - : Natural → ∀(a : Type) → (Natural → a) → List a - = λ(n : Natural) - → λ(a : Type) - → λ(f : Natural → a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - { index : Natural, value : {} } - ( List/indexed - {} - ( List/build - {} - ( λ(list : Type) - → λ(cons : {} → list → list) - → Natural/fold n list (cons {=}) - ) - ) +let generate + : Natural → ∀(a : Type) → (Natural → a) → List a + = λ(n : Natural) + → λ(a : Type) + → λ(f : Natural → a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + { index : Natural, value : {} } + ( List/indexed + {} + ( List/build + {} + ( λ(list : Type) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) ) - list - (λ(x : { index : Natural, value : {} }) → cons (f x.index)) + ) ) + list + (λ(x : { index : Natural, value : {} }) → cons (f x.index)) + ) in generate diff --git a/Prelude/List/indexed b/Prelude/List/indexed index 06bb22714..ffcd28d17 100644 --- a/Prelude/List/indexed +++ b/Prelude/List/indexed @@ -14,8 +14,8 @@ Examples: = [] : List { index : Natural, value : Bool } ``` -} - let indexed - : ∀(a : Type) → List a → List { index : Natural, value : a } - = List/indexed +let indexed + : ∀(a : Type) → List a → List { index : Natural, value : a } + = List/indexed in indexed diff --git a/Prelude/List/iterate b/Prelude/List/iterate index fd6e11d00..4c389051d 100644 --- a/Prelude/List/iterate +++ b/Prelude/List/iterate @@ -12,32 +12,32 @@ Examples: = [] : List Natural ``` -} - let iterate - : Natural → ∀(a : Type) → (a → a) → a → List a - = λ(n : Natural) - → λ(a : Type) - → λ(f : a → a) - → λ(x : a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - { index : Natural, value : {} } - ( List/indexed - {} - ( List/build - {} - ( λ(list : Type) - → λ(cons : {} → list → list) - → Natural/fold n list (cons {=}) - ) - ) - ) - list - ( λ(y : { index : Natural, value : {} }) - → cons (Natural/fold y.index a f x) +let iterate + : Natural → ∀(a : Type) → (a → a) → a → List a + = λ(n : Natural) + → λ(a : Type) + → λ(f : a → a) + → λ(x : a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + { index : Natural, value : {} } + ( List/indexed + {} + ( List/build + {} + ( λ(list : Type) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) ) + ) + ) + list + ( λ(y : { index : Natural, value : {} }) + → cons (Natural/fold y.index a f x) ) + ) in iterate diff --git a/Prelude/List/map b/Prelude/List/map index e82c40de4..04196db0a 100644 --- a/Prelude/List/map +++ b/Prelude/List/map @@ -11,17 +11,17 @@ Examples: = [] : List Bool ``` -} - let map - : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b - = λ(a : Type) - → λ(b : Type) - → λ(f : a → b) - → λ(xs : List a) - → List/build - b - ( λ(list : Type) - → λ(cons : b → list → list) - → List/fold a xs list (λ(x : a) → cons (f x)) - ) +let map + : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b + = λ(a : Type) + → λ(b : Type) + → λ(f : a → b) + → λ(xs : List a) + → List/build + b + ( λ(list : Type) + → λ(cons : b → list → list) + → List/fold a xs list (λ(x : a) → cons (f x)) + ) in map diff --git a/Prelude/List/null b/Prelude/List/null index e38f92557..12bb8f347 100644 --- a/Prelude/List/null +++ b/Prelude/List/null @@ -9,8 +9,8 @@ Examples: ./null Natural ([] : List Natural) = True ``` -} - let null - : ∀(a : Type) → List a → Bool - = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs) +let null + : ∀(a : Type) → List a → Bool + = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs) in null diff --git a/Prelude/List/package.dhall b/Prelude/List/package.dhall index efd30eeef..5b50b412a 100644 --- a/Prelude/List/package.dhall +++ b/Prelude/List/package.dhall @@ -1,58 +1,58 @@ { all = - ./all sha256:7ac5bb6f77e9ffe9e2356d90968d39764a9a32f75980206e6b12f815bb83dd15 + ./all sha256:7ac5bb6f77e9ffe9e2356d90968d39764a9a32f75980206e6b12f815bb83dd15 ? ./all , any = - ./any sha256:b8e9e13b25e799f342a81f6eda4075906eb1a19dfdcb10a0ca25925eba4033b8 + ./any sha256:b8e9e13b25e799f342a81f6eda4075906eb1a19dfdcb10a0ca25925eba4033b8 ? ./any , build = - ./build sha256:8cf73fc1e115cfcb79bb9cd490bfcbd45c824e93c57a0e64c86c0c72e9ebbe42 + ./build sha256:8cf73fc1e115cfcb79bb9cd490bfcbd45c824e93c57a0e64c86c0c72e9ebbe42 ? ./build , concat = - ./concat sha256:54e43278be13276e03bd1afa89e562e94a0a006377ebea7db14c7562b0de292b + ./concat sha256:54e43278be13276e03bd1afa89e562e94a0a006377ebea7db14c7562b0de292b ? ./concat , concatMap = - ./concatMap sha256:3b2167061d11fda1e4f6de0522cbe83e0d5ac4ef5ddf6bb0b2064470c5d3fb64 + ./concatMap sha256:3b2167061d11fda1e4f6de0522cbe83e0d5ac4ef5ddf6bb0b2064470c5d3fb64 ? ./concatMap , filter = - ./filter sha256:8ebfede5bbfe09675f246c33eb83964880ac615c4b1be8d856076fdbc4b26ba6 + ./filter sha256:8ebfede5bbfe09675f246c33eb83964880ac615c4b1be8d856076fdbc4b26ba6 ? ./filter , fold = - ./fold sha256:10bb945c25ab3943bd9df5a32e633cbfae112b7d3af38591784687e436a8d814 + ./fold sha256:10bb945c25ab3943bd9df5a32e633cbfae112b7d3af38591784687e436a8d814 ? ./fold , generate = - ./generate sha256:78ff1ad96c08b88a8263eea7bc8381c078225cfcb759c496f792edb5a5e0b1a4 + ./generate sha256:78ff1ad96c08b88a8263eea7bc8381c078225cfcb759c496f792edb5a5e0b1a4 ? ./generate , head = - ./head sha256:0d2e65ba0aea908377e46d22020dc3ad970284f4ee4eb8e6b8c51e53038c0026 + ./head sha256:0d2e65ba0aea908377e46d22020dc3ad970284f4ee4eb8e6b8c51e53038c0026 ? ./head , indexed = - ./indexed sha256:58bb44457fa81adf26f5123c1b2e8bef0c5aa22dac5fa5ebdfb7da84563b027f + ./indexed sha256:58bb44457fa81adf26f5123c1b2e8bef0c5aa22dac5fa5ebdfb7da84563b027f ? ./indexed , iterate = - ./iterate sha256:e4999ccce190a2e2a6ab9cb188e3af6c40df474087827153005293f11bfe1d26 + ./iterate sha256:e4999ccce190a2e2a6ab9cb188e3af6c40df474087827153005293f11bfe1d26 ? ./iterate , last = - ./last sha256:741226b741af152a1638491cdff7f3aa74baf080ada2e63429483f3d195a984d + ./last sha256:741226b741af152a1638491cdff7f3aa74baf080ada2e63429483f3d195a984d ? ./last , length = - ./length sha256:42c6812c7a9e3c6e6fad88f77c5b3849503964e071cb784e22c38c888a401461 + ./length sha256:42c6812c7a9e3c6e6fad88f77c5b3849503964e071cb784e22c38c888a401461 ? ./length , map = - ./map sha256:dd845ffb4568d40327f2a817eb42d1c6138b929ca758d50bc33112ef3c885680 + ./map sha256:dd845ffb4568d40327f2a817eb42d1c6138b929ca758d50bc33112ef3c885680 ? ./map , null = - ./null sha256:2338e39637e9a50d66ae1482c0ed559bbcc11e9442bfca8f8c176bbcd9c4fc80 + ./null sha256:2338e39637e9a50d66ae1482c0ed559bbcc11e9442bfca8f8c176bbcd9c4fc80 ? ./null , replicate = - ./replicate sha256:d4250b45278f2d692302489ac3e78280acb238d27541c837ce46911ff3baa347 + ./replicate sha256:d4250b45278f2d692302489ac3e78280acb238d27541c837ce46911ff3baa347 ? ./replicate , reverse = - ./reverse sha256:ad99d224d61852de6696da5a7d04c98dbe676fe67d5e4ef4f19e9aaa27006e9d + ./reverse sha256:ad99d224d61852de6696da5a7d04c98dbe676fe67d5e4ef4f19e9aaa27006e9d ? ./reverse , shifted = - ./shifted sha256:54fb22c7e952ebce1cfc0fcdd33ce4cfa817bff9d6564af268dea6685f8b5dfe + ./shifted sha256:54fb22c7e952ebce1cfc0fcdd33ce4cfa817bff9d6564af268dea6685f8b5dfe ? ./shifted , unzip = - ./unzip sha256:4d6003e9e683a289fe33f4c90f958eb1e08ea0bbb474210fcd90d1885c9660e9 + ./unzip sha256:4d6003e9e683a289fe33f4c90f958eb1e08ea0bbb474210fcd90d1885c9660e9 ? ./unzip } diff --git a/Prelude/List/replicate b/Prelude/List/replicate index 3f2fede69..42c8b0f85 100644 --- a/Prelude/List/replicate +++ b/Prelude/List/replicate @@ -9,16 +9,16 @@ Examples: ./replicate 0 Natural 1 = [] : List Natural ``` -} - let replicate - : Natural → ∀(a : Type) → a → List a - = λ(n : Natural) - → λ(a : Type) - → λ(x : a) - → List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → Natural/fold n list (cons x) - ) +let replicate + : Natural → ∀(a : Type) → a → List a + = λ(n : Natural) + → λ(a : Type) + → λ(x : a) + → List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → Natural/fold n list (cons x) + ) in replicate diff --git a/Prelude/List/shifted b/Prelude/List/shifted index 80551dc41..3884e8057 100644 --- a/Prelude/List/shifted +++ b/Prelude/List/shifted @@ -35,56 +35,52 @@ Bool = [] : List { index : Natural, value : Bool } ``` -} - let shifted - : ∀(a : Type) - → List (List { index : Natural, value : a }) - → List { index : Natural, value : a } - = λ(a : Type) - → λ(kvss : List (List { index : Natural, value : a })) - → List/build - { index : Natural, value : a } - ( λ(list : Type) - → λ(cons : { index : Natural, value : a } → list → list) - → λ(nil : list) - → let result = - List/fold - (List { index : Natural, value : a }) - kvss - { count : Natural, diff : Natural → list } - ( λ(kvs : List { index : Natural, value : a }) - → λ(y : { count : Natural, diff : Natural → list }) - → let length = - List/length - { index : Natural, value : a } - kvs - - in { count = - y.count + length - , diff = - λ(n : Natural) - → List/fold - { index : Natural, value : a } - kvs - list - ( λ ( kvOld - : { index : Natural, value : a } - ) - → λ(z : list) - → let kvNew = - { index = - kvOld.index + n - , value = - kvOld.value - } - - in cons kvNew z - ) - (y.diff (n + length)) - } - ) - { count = 0, diff = λ(_ : Natural) → nil } - - in result.diff 0 - ) +let shifted + : ∀(a : Type) + → List (List { index : Natural, value : a }) + → List { index : Natural, value : a } + = λ(a : Type) + → λ(kvss : List (List { index : Natural, value : a })) + → List/build + { index : Natural, value : a } + ( λ(list : Type) + → λ(cons : { index : Natural, value : a } → list → list) + → λ(nil : list) + → let result = + List/fold + (List { index : Natural, value : a }) + kvss + { count : Natural, diff : Natural → list } + ( λ(kvs : List { index : Natural, value : a }) + → λ(y : { count : Natural, diff : Natural → list }) + → let length = + List/length { index : Natural, value : a } kvs + + in { count = + y.count + length + , diff = + λ(n : Natural) + → List/fold + { index : Natural, value : a } + kvs + list + ( λ(kvOld : { index : Natural, value : a }) + → λ(z : list) + → let kvNew = + { index = + kvOld.index + n + , value = + kvOld.value + } + + in cons kvNew z + ) + (y.diff (n + length)) + } + ) + { count = 0, diff = λ(_ : Natural) → nil } + + in result.diff 0 + ) in shifted diff --git a/Prelude/List/unzip b/Prelude/List/unzip index 8293ced27..7ea74aa41 100644 --- a/Prelude/List/unzip +++ b/Prelude/List/unzip @@ -20,36 +20,36 @@ Bool = { _1 = [] : List Text, _2 = [] : List Bool } ``` -} - let unzip - : ∀(a : Type) - → ∀(b : Type) - → List { _1 : a, _2 : b } - → { _1 : List a, _2 : List b } - = λ(a : Type) - → λ(b : Type) - → λ(xs : List { _1 : a, _2 : b }) - → { _1 = - List/build - a - ( λ(list : Type) - → λ(cons : a → list → list) - → List/fold - { _1 : a, _2 : b } - xs - list - (λ(x : { _1 : a, _2 : b }) → cons x._1) - ) - , _2 = - List/build - b - ( λ(list : Type) - → λ(cons : b → list → list) - → List/fold - { _1 : a, _2 : b } - xs - list - (λ(x : { _1 : a, _2 : b }) → cons x._2) - ) - } +let unzip + : ∀(a : Type) + → ∀(b : Type) + → List { _1 : a, _2 : b } + → { _1 : List a, _2 : List b } + = λ(a : Type) + → λ(b : Type) + → λ(xs : List { _1 : a, _2 : b }) + → { _1 = + List/build + a + ( λ(list : Type) + → λ(cons : a → list → list) + → List/fold + { _1 : a, _2 : b } + xs + list + (λ(x : { _1 : a, _2 : b }) → cons x._1) + ) + , _2 = + List/build + b + ( λ(list : Type) + → λ(cons : b → list → list) + → List/fold + { _1 : a, _2 : b } + xs + list + (λ(x : { _1 : a, _2 : b }) → cons x._2) + ) + } in unzip diff --git a/Prelude/Natural/build b/Prelude/Natural/build index a01ef7ebd..24013888f 100644 --- a/Prelude/Natural/build +++ b/Prelude/Natural/build @@ -21,13 +21,13 @@ Examples: = 0 ``` -} - let build - : ( ∀(natural : Type) - → ∀(succ : natural → natural) - → ∀(zero : natural) - → natural - ) - → Natural - = Natural/build +let build + : ( ∀(natural : Type) + → ∀(succ : natural → natural) + → ∀(zero : natural) + → natural + ) + → Natural + = Natural/build in build diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate index c90612f62..1de7af429 100644 --- a/Prelude/Natural/enumerate +++ b/Prelude/Natural/enumerate @@ -10,27 +10,27 @@ Examples: ./enumerate 0 = [] : List Natural ``` -} - let enumerate - : Natural → List Natural - = λ(n : Natural) - → List/build - Natural - ( λ(list : Type) - → λ(cons : Natural → list → list) - → List/fold - { index : Natural, value : {} } - ( List/indexed - {} - ( List/build - {} - ( λ(list : Type) - → λ(cons : {} → list → list) - → Natural/fold n list (cons {=}) - ) - ) +let enumerate + : Natural → List Natural + = λ(n : Natural) + → List/build + Natural + ( λ(list : Type) + → λ(cons : Natural → list → list) + → List/fold + { index : Natural, value : {} } + ( List/indexed + {} + ( List/build + {} + ( λ(list : Type) + → λ(cons : {} → list → list) + → Natural/fold n list (cons {=}) ) - list - (λ(x : { index : Natural, value : {} }) → cons x.index) + ) ) + list + (λ(x : { index : Natural, value : {} }) → cons x.index) + ) in enumerate diff --git a/Prelude/Natural/fold b/Prelude/Natural/fold index 2150d3edc..ed0c77a3e 100644 --- a/Prelude/Natural/fold +++ b/Prelude/Natural/fold @@ -22,12 +22,12 @@ Examples: → succ (succ (succ zero)) ``` -} - let fold - : Natural - → ∀(natural : Type) - → ∀(succ : natural → natural) - → ∀(zero : natural) - → natural - = Natural/fold +let fold + : Natural + → ∀(natural : Type) + → ∀(succ : natural → natural) + → ∀(zero : natural) + → natural + = Natural/fold in fold diff --git a/Prelude/Natural/package.dhall b/Prelude/Natural/package.dhall index 4aef3e56c..ccf0bffb4 100644 --- a/Prelude/Natural/package.dhall +++ b/Prelude/Natural/package.dhall @@ -1,34 +1,34 @@ { build = - ./build sha256:e7e25e6c4f1d8e573606ed1bef725396ac2de5c68f7c5d329ffc5822085b984c + ./build sha256:e7e25e6c4f1d8e573606ed1bef725396ac2de5c68f7c5d329ffc5822085b984c ? ./build , enumerate = - ./enumerate sha256:0cf083980a752b21ce0df9fc2222a4c139f50909e2353576e26a191002aa1ce3 + ./enumerate sha256:0cf083980a752b21ce0df9fc2222a4c139f50909e2353576e26a191002aa1ce3 ? ./enumerate , even = - ./even sha256:b85b8b56892dfef881e1c0e79eade0b949528f792aac0ea42432b315ede4ee66 + ./even sha256:b85b8b56892dfef881e1c0e79eade0b949528f792aac0ea42432b315ede4ee66 ? ./even , fold = - ./fold sha256:fd01c931e585a8f5fd049af7b076b862ea164f1813b34800c7616a49e549ee06 + ./fold sha256:fd01c931e585a8f5fd049af7b076b862ea164f1813b34800c7616a49e549ee06 ? ./fold , isZero = - ./isZero sha256:1be98236800ed2d5cff44f16ca02b34b0c37dfa239d9e0d63d9d2c6eeae3d1d1 + ./isZero sha256:1be98236800ed2d5cff44f16ca02b34b0c37dfa239d9e0d63d9d2c6eeae3d1d1 ? ./isZero , odd = - ./odd sha256:ab3c729262c642ec1cdb72a81e910fcfaf2aea13e3961d0bf1bec83efea5aac5 + ./odd sha256:ab3c729262c642ec1cdb72a81e910fcfaf2aea13e3961d0bf1bec83efea5aac5 ? ./odd , product = - ./product sha256:e3e6fd76207875b81d39f79fdbc90b5e640444c04fb3d84c2c9326748f0b26e6 + ./product sha256:e3e6fd76207875b81d39f79fdbc90b5e640444c04fb3d84c2c9326748f0b26e6 ? ./product , sum = - ./sum sha256:33f7f4c3aff62e5ecf4848f964363133452d420dcde045784518fb59fa970037 + ./sum sha256:33f7f4c3aff62e5ecf4848f964363133452d420dcde045784518fb59fa970037 ? ./sum , show = - ./show sha256:684ed560ad86f438efdea229eca122c29e8e14f397ed32ec97148d578ca5aa21 + ./show sha256:684ed560ad86f438efdea229eca122c29e8e14f397ed32ec97148d578ca5aa21 ? ./show , toDouble = - ./toDouble sha256:d5eb52143dcd35b46a6f0cdb2d3cbf31a14b6daeba56e29066f8e344c9fb6e81 + ./toDouble sha256:d5eb52143dcd35b46a6f0cdb2d3cbf31a14b6daeba56e29066f8e344c9fb6e81 ? ./toDouble , toInteger = - ./toInteger sha256:160d2d278619f3da34a1f4f02e739a447e4f2aa5a2978c45b710515b41491e1f + ./toInteger sha256:160d2d278619f3da34a1f4f02e739a447e4f2aa5a2978c45b710515b41491e1f ? ./toInteger } diff --git a/Prelude/Natural/product b/Prelude/Natural/product index dcc5235cd..4642a8029 100644 --- a/Prelude/Natural/product +++ b/Prelude/Natural/product @@ -9,14 +9,9 @@ Examples: ./product ([] : List Natural) = 1 ``` -} - let product - : List Natural → Natural - = λ(xs : List Natural) - → List/fold - Natural - xs - Natural - (λ(l : Natural) → λ(r : Natural) → l * r) - 1 +let product + : List Natural → Natural + = λ(xs : List Natural) + → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) 1 in product diff --git a/Prelude/Natural/sum b/Prelude/Natural/sum index 0f0f69735..c09e20690 100644 --- a/Prelude/Natural/sum +++ b/Prelude/Natural/sum @@ -9,14 +9,9 @@ Examples: ./sum ([] : List Natural) = 0 ``` -} - let sum - : List Natural → Natural - = λ(xs : List Natural) - → List/fold - Natural - xs - Natural - (λ(l : Natural) → λ(r : Natural) → l + r) - 0 +let sum + : List Natural → Natural + = λ(xs : List Natural) + → List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) 0 in sum diff --git a/Prelude/Natural/toDouble b/Prelude/Natural/toDouble index 12f9392a2..4fe2c014e 100644 --- a/Prelude/Natural/toDouble +++ b/Prelude/Natural/toDouble @@ -9,8 +9,8 @@ Examples: ./toDouble 0 = 0.0 ``` -} - let toDouble - : Natural → Double - = λ(n : Natural) → Integer/toDouble (Natural/toInteger n) +let toDouble + : Natural → Double + = λ(n : Natural) → Integer/toDouble (Natural/toInteger n) in toDouble diff --git a/Prelude/Optional/all b/Prelude/Optional/all index 0db2c8f2f..b24e4eeb4 100644 --- a/Prelude/Optional/all +++ b/Prelude/Optional/all @@ -10,11 +10,11 @@ Examples: ./all Natural Natural/even (None Natural) = True ``` -} - let all - : ∀(a : Type) → (a → Bool) → Optional a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : Optional a) - → Optional/fold a xs Bool f True +let all + : ∀(a : Type) → (a → Bool) → Optional a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : Optional a) + → Optional/fold a xs Bool f True in all diff --git a/Prelude/Optional/any b/Prelude/Optional/any index 172cebc15..41592d121 100644 --- a/Prelude/Optional/any +++ b/Prelude/Optional/any @@ -10,11 +10,11 @@ Examples: ./any Natural Natural/even (None Natural) = False ``` -} - let any - : ∀(a : Type) → (a → Bool) → Optional a → Bool - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : Optional a) - → Optional/fold a xs Bool f False +let any + : ∀(a : Type) → (a → Bool) → Optional a → Bool + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : Optional a) + → Optional/fold a xs Bool f False in any diff --git a/Prelude/Optional/build b/Prelude/Optional/build index dde5fa698..5b556aee4 100644 --- a/Prelude/Optional/build +++ b/Prelude/Optional/build @@ -23,14 +23,14 @@ Natural = None Natural ``` -} - let build - : ∀(a : Type) - → ( ∀(optional : Type) - → ∀(some : a → optional) - → ∀(none : optional) - → optional - ) - → Optional a - = Optional/build +let build + : ∀(a : Type) + → ( ∀(optional : Type) + → ∀(some : a → optional) + → ∀(none : optional) + → optional + ) + → Optional a + = Optional/build in build diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat index 8bbd36f67..652d1780d 100644 --- a/Prelude/Optional/concat +++ b/Prelude/Optional/concat @@ -14,15 +14,15 @@ Examples: = None Natural ``` -} - let concat - : ∀(a : Type) → Optional (Optional a) → Optional a - = λ(a : Type) - → λ(x : Optional (Optional a)) - → Optional/fold - (Optional a) - x - (Optional a) - (λ(y : Optional a) → y) - (None a) +let concat + : ∀(a : Type) → Optional (Optional a) → Optional a + = λ(a : Type) + → λ(x : Optional (Optional a)) + → Optional/fold + (Optional a) + x + (Optional a) + (λ(y : Optional a) → y) + (None a) in concat diff --git a/Prelude/Optional/filter b/Prelude/Optional/filter index 3c0d4eb5e..85ff36453 100644 --- a/Prelude/Optional/filter +++ b/Prelude/Optional/filter @@ -11,22 +11,22 @@ Examples: = None Natural ``` -} - let filter - : ∀(a : Type) → (a → Bool) → Optional a → Optional a - = λ(a : Type) - → λ(f : a → Bool) - → λ(xs : Optional a) - → Optional/build +let filter + : ∀(a : Type) → (a → Bool) → Optional a → Optional a + = λ(a : Type) + → λ(f : a → Bool) + → λ(xs : Optional a) + → Optional/build + a + ( λ(optional : Type) + → λ(some : a → optional) + → λ(none : optional) + → Optional/fold a - ( λ(optional : Type) - → λ(some : a → optional) - → λ(none : optional) - → Optional/fold - a - xs - optional - (λ(x : a) → if f x then some x else none) - none - ) + xs + optional + (λ(x : a) → if f x then some x else none) + none + ) in filter diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold index 602fba21d..ece49152a 100644 --- a/Prelude/Optional/fold +++ b/Prelude/Optional/fold @@ -9,13 +9,13 @@ Examples: ./fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 = 0 ``` -} - let fold - : ∀(a : Type) - → Optional a - → ∀(optional : Type) - → ∀(some : a → optional) - → ∀(none : optional) - → optional - = Optional/fold +let fold + : ∀(a : Type) + → Optional a + → ∀(optional : Type) + → ∀(some : a → optional) + → ∀(none : optional) + → optional + = Optional/fold in fold diff --git a/Prelude/Optional/head b/Prelude/Optional/head index 9cbce3ca3..67ff510e7 100644 --- a/Prelude/Optional/head +++ b/Prelude/Optional/head @@ -11,18 +11,18 @@ Examples: ./head Natural ([] : List (Optional Natural)) = None Natural ``` -} - let head - : ∀(a : Type) → List (Optional a) → Optional a - = λ(a : Type) - → λ(xs : List (Optional a)) - → List/fold - (Optional a) - xs - (Optional a) - ( λ(l : Optional a) - → λ(r : Optional a) - → Optional/fold a l (Optional a) (λ(x : a) → Some x) r - ) - (None a) +let head + : ∀(a : Type) → List (Optional a) → Optional a + = λ(a : Type) + → λ(xs : List (Optional a)) + → List/fold + (Optional a) + xs + (Optional a) + ( λ(l : Optional a) + → λ(r : Optional a) + → Optional/fold a l (Optional a) (λ(x : a) → Some x) r + ) + (None a) in head diff --git a/Prelude/Optional/last b/Prelude/Optional/last index 8c70d9ef6..2d1431a1b 100644 --- a/Prelude/Optional/last +++ b/Prelude/Optional/last @@ -11,18 +11,18 @@ Examples: ./last Natural ([] : List (Optional Natural)) = None Natural ``` -} - let last - : ∀(a : Type) → List (Optional a) → Optional a - = λ(a : Type) - → λ(xs : List (Optional a)) - → List/fold - (Optional a) - xs - (Optional a) - ( λ(l : Optional a) - → λ(r : Optional a) - → Optional/fold a r (Optional a) (λ(x : a) → Some x) l - ) - (None a) +let last + : ∀(a : Type) → List (Optional a) → Optional a + = λ(a : Type) + → λ(xs : List (Optional a)) + → List/fold + (Optional a) + xs + (Optional a) + ( λ(l : Optional a) + → λ(r : Optional a) + → Optional/fold a r (Optional a) (λ(x : a) → Some x) l + ) + (None a) in last diff --git a/Prelude/Optional/length b/Prelude/Optional/length index c8df433a6..c345fc6b7 100644 --- a/Prelude/Optional/length +++ b/Prelude/Optional/length @@ -9,10 +9,10 @@ Examples: ./length Natural (None Natural) = 0 ``` -} - let length - : ∀(a : Type) → Optional a → Natural - = λ(a : Type) - → λ(xs : Optional a) - → Optional/fold a xs Natural (λ(_ : a) → 1) 0 +let length + : ∀(a : Type) → Optional a → Natural + = λ(a : Type) + → λ(xs : Optional a) + → Optional/fold a xs Natural (λ(_ : a) → 1) 0 in length diff --git a/Prelude/Optional/map b/Prelude/Optional/map index d08329e0b..f8106d80c 100644 --- a/Prelude/Optional/map +++ b/Prelude/Optional/map @@ -9,12 +9,12 @@ Examples: ./map Natural Bool Natural/even (None Natural) = None Bool ``` -} - let map - : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b - = λ(a : Type) - → λ(b : Type) - → λ(f : a → b) - → λ(o : Optional a) - → Optional/fold a o (Optional b) (λ(x : a) → Some (f x)) (None b) +let map + : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b + = λ(a : Type) + → λ(b : Type) + → λ(f : a → b) + → λ(o : Optional a) + → Optional/fold a o (Optional b) (λ(x : a) → Some (f x)) (None b) in map diff --git a/Prelude/Optional/null b/Prelude/Optional/null index 6854edb13..1a246ff87 100644 --- a/Prelude/Optional/null +++ b/Prelude/Optional/null @@ -9,10 +9,10 @@ Examples: ./null Natural (None Natural) = True ``` -} - let null - : ∀(a : Type) → Optional a → Bool - = λ(a : Type) - → λ(xs : Optional a) - → Optional/fold a xs Bool (λ(_ : a) → False) True +let null + : ∀(a : Type) → Optional a → Bool + = λ(a : Type) + → λ(xs : Optional a) + → Optional/fold a xs Bool (λ(_ : a) → False) True in null diff --git a/Prelude/Optional/package.dhall b/Prelude/Optional/package.dhall index 80c81fecd..688ed4ae4 100644 --- a/Prelude/Optional/package.dhall +++ b/Prelude/Optional/package.dhall @@ -1,40 +1,40 @@ { all = - ./all sha256:b9b015fe8be14da940901aa1510ee1d5e205df37ee651c32ac975a799782c410 + ./all sha256:b9b015fe8be14da940901aa1510ee1d5e205df37ee651c32ac975a799782c410 ? ./all , any = - ./any sha256:0a637c0f2cc7d30b8f0bca021d2ee1ad1213fb9d9712c669b29feab66a590eaf + ./any sha256:0a637c0f2cc7d30b8f0bca021d2ee1ad1213fb9d9712c669b29feab66a590eaf ? ./any , build = - ./build sha256:f331299d1279cfb88dd25a5acfdd64130900991b6154239ad343a2883f6eb50c + ./build sha256:f331299d1279cfb88dd25a5acfdd64130900991b6154239ad343a2883f6eb50c ? ./build , concat = - ./concat sha256:b49a3b7dc49eb83d150977caa5ae347be1cbbe14e3b6d0e07349bd2e5f707d69 + ./concat sha256:b49a3b7dc49eb83d150977caa5ae347be1cbbe14e3b6d0e07349bd2e5f707d69 ? ./concat , filter = - ./filter sha256:b3d5e19a6cec592a76c12167a9e5e1e76649e776229d70a11c77b76cd29f617e + ./filter sha256:b3d5e19a6cec592a76c12167a9e5e1e76649e776229d70a11c77b76cd29f617e ? ./filter , fold = - ./fold sha256:62139ff410ca84302acebe763a8a1794420dd472d907384c7fb80df2a2180302 + ./fold sha256:62139ff410ca84302acebe763a8a1794420dd472d907384c7fb80df2a2180302 ? ./fold , head = - ./head sha256:b0b5d257294515f1de35f24fa83e54d7f1d5ebca9c3c1fc903a80ab40e19b3a6 + ./head sha256:b0b5d257294515f1de35f24fa83e54d7f1d5ebca9c3c1fc903a80ab40e19b3a6 ? ./head , last = - ./last sha256:f839221a8a04adae6c501458eb264e7f4e375a1facb294cb80caacfd012a6765 + ./last sha256:f839221a8a04adae6c501458eb264e7f4e375a1facb294cb80caacfd012a6765 ? ./last , length = - ./length sha256:722a3754a411c053f006a32c506a6d1b14869c2ab799169df9cdac346edf07d3 + ./length sha256:722a3754a411c053f006a32c506a6d1b14869c2ab799169df9cdac346edf07d3 ? ./length , map = - ./map sha256:e7f44219250b89b094fbf9996e04b5daafc0902d864113420072ae60706ac73d + ./map sha256:e7f44219250b89b094fbf9996e04b5daafc0902d864113420072ae60706ac73d ? ./map , null = - ./null sha256:efc43103e49b56c5bf089db8e0365bbfc455b8a2f0dc6ee5727a3586f85969fd + ./null sha256:efc43103e49b56c5bf089db8e0365bbfc455b8a2f0dc6ee5727a3586f85969fd ? ./null , toList = - ./toList sha256:390fe99619e9a25e71a253a2b33011f9e5fa26a7d990795205543d1edd72ce5b + ./toList sha256:390fe99619e9a25e71a253a2b33011f9e5fa26a7d990795205543d1edd72ce5b ? ./toList , unzip = - ./unzip sha256:7b517bc2a8a4dbec044c6bea5e059cafde5a0cb1d3a5e7d13d346c9327a00f30 + ./unzip sha256:7b517bc2a8a4dbec044c6bea5e059cafde5a0cb1d3a5e7d13d346c9327a00f30 ? ./unzip } diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList index 6dc7ccb84..c6eb80324 100644 --- a/Prelude/Optional/toList +++ b/Prelude/Optional/toList @@ -9,10 +9,10 @@ Examples: ./toList Natural (None Natural) = [] : List Natural ``` -} - let toList - : ∀(a : Type) → Optional a → List a - = λ(a : Type) - → λ(o : Optional a) - → Optional/fold a o (List a) (λ(x : a) → [ x ] : List a) ([] : List a) +let toList + : ∀(a : Type) → Optional a → List a + = λ(a : Type) + → λ(o : Optional a) + → Optional/fold a o (List a) (λ(x : a) → [ x ] : List a) ([] : List a) in toList diff --git a/Prelude/Optional/unzip b/Prelude/Optional/unzip index af4b99f99..862996032 100644 --- a/Prelude/Optional/unzip +++ b/Prelude/Optional/unzip @@ -11,28 +11,28 @@ Examples: = { _1 = None Text, _2 = None Bool } ``` -} - let unzip - : ∀(a : Type) - → ∀(b : Type) - → Optional { _1 : a, _2 : b } - → { _1 : Optional a, _2 : Optional b } - = λ(a : Type) - → λ(b : Type) - → λ(xs : Optional { _1 : a, _2 : b }) - → { _1 = - Optional/fold - { _1 : a, _2 : b } - xs - (Optional a) - (λ(x : { _1 : a, _2 : b }) → Some x._1) - (None a) - , _2 = - Optional/fold - { _1 : a, _2 : b } - xs - (Optional b) - (λ(x : { _1 : a, _2 : b }) → Some x._2) - (None b) - } +let unzip + : ∀(a : Type) + → ∀(b : Type) + → Optional { _1 : a, _2 : b } + → { _1 : Optional a, _2 : Optional b } + = λ(a : Type) + → λ(b : Type) + → λ(xs : Optional { _1 : a, _2 : b }) + → { _1 = + Optional/fold + { _1 : a, _2 : b } + xs + (Optional a) + (λ(x : { _1 : a, _2 : b }) → Some x._1) + (None a) + , _2 = + Optional/fold + { _1 : a, _2 : b } + xs + (Optional b) + (λ(x : { _1 : a, _2 : b }) → Some x._2) + (None b) + } in unzip diff --git a/Prelude/Text/concat b/Prelude/Text/concat index 7f14e5ace..de7573c6f 100644 --- a/Prelude/Text/concat +++ b/Prelude/Text/concat @@ -9,9 +9,9 @@ Examples: ./concat ([] : List Text) = "" ``` -} - let concat - : List Text → Text - = λ(xs : List Text) - → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) "" +let concat + : List Text → Text + = λ(xs : List Text) + → List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) "" in concat diff --git a/Prelude/Text/concatMap b/Prelude/Text/concatMap index 86db318e3..e2aa53667 100644 --- a/Prelude/Text/concatMap +++ b/Prelude/Text/concatMap @@ -11,11 +11,11 @@ Examples: = "" ``` -} - let concatMap - : ∀(a : Type) → (a → Text) → List a → Text - = λ(a : Type) - → λ(f : a → Text) - → λ(xs : List a) - → List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) "" +let concatMap + : ∀(a : Type) → (a → Text) → List a → Text + = λ(a : Type) + → λ(f : a → Text) + → λ(xs : List a) + → List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) "" in concatMap diff --git a/Prelude/Text/package.dhall b/Prelude/Text/package.dhall index 5c4debcb6..9536a2f15 100644 --- a/Prelude/Text/package.dhall +++ b/Prelude/Text/package.dhall @@ -1,16 +1,16 @@ { concat = - ./concat sha256:35e20d9403fbadb1a0061edb84e076ed56313709fa4bc8124d86ff54896f20ac + ./concat sha256:35e20d9403fbadb1a0061edb84e076ed56313709fa4bc8124d86ff54896f20ac ? ./concat , concatMap = - ./concatMap sha256:175d893ad7f2b2c05fff9e32f0d9cbadc7f5fce57945071508cf3603f8aa298e + ./concatMap sha256:175d893ad7f2b2c05fff9e32f0d9cbadc7f5fce57945071508cf3603f8aa298e ? ./concatMap , concatMapSep = - ./concatMapSep sha256:46b81a9e211fb8278bf2793e75e8175fef79e0e3e478ef1016e3233ecc2ddfe6 + ./concatMapSep sha256:46b81a9e211fb8278bf2793e75e8175fef79e0e3e478ef1016e3233ecc2ddfe6 ? ./concatMapSep , concatSep = - ./concatSep sha256:d28e61f5057a240e857e09dba1b040fa3477bddb9659c5606c760852a9165890 + ./concatSep sha256:d28e61f5057a240e857e09dba1b040fa3477bddb9659c5606c760852a9165890 ? ./concatSep , show = - ./show sha256:c9dc5de3e5f32872dbda57166804865e5e80785abe358ff61f1d8ac45f1f4784 + ./show sha256:c9dc5de3e5f32872dbda57166804865e5e80785abe358ff61f1d8ac45f1f4784 ? ./show } diff --git a/Prelude/package.dhall b/Prelude/package.dhall index f851d88d9..d6d1be094 100644 --- a/Prelude/package.dhall +++ b/Prelude/package.dhall @@ -1,28 +1,28 @@ -{ `Bool` = +{ Bool = ./Bool/package.dhall sha256:7ee950e7c2142be5923f76d00263e536b71d96cb9c190d7743c1679501ddeb0a ? ./Bool/package.dhall -, `Double` = +, Double = ./Double/package.dhall sha256:b8d20ab3216083622ae371fb42a6732bc67bb2d66e84989c8ddba7556a336cf7 ? ./Double/package.dhall , Function = ./Function/package.dhall sha256:74c3822b98b9d37f9f820af8e1a7ee790bcfac03050eabd45af4a255fb93e026 ? ./Function/package.dhall -, `Integer` = +, Integer = ./Integer/package.dhall sha256:eb464566d3192dd16ce915a9bd874aaaad612d5c69beb356e5b7d2e0c4949dcf ? ./Integer/package.dhall -, `List` = +, List = ./List/package.dhall sha256:108be3af5ebd465f7091039f2216c433e65ae5d25556a9a71786dd84d33ef49a ? ./List/package.dhall -, `Natural` = +, Natural = ./Natural/package.dhall sha256:fe08155c3a04500df847ca94d013ecd3dfc73ab5c136109b2414fce3ec42b63a ? ./Natural/package.dhall -, `Optional` = +, Optional = ./Optional/package.dhall sha256:36a366af67a3c26cd5d196e095d3023f18953c5b5db3a03956fa554609e5442a ? ./Optional/package.dhall , JSON = ./JSON/package.dhall sha256:7f0c25a292e5d34ddfbbf3f6d90505567382f95d822b04f5810745f81ab1ef35 ? ./JSON/package.dhall -, `Text` = +, Text = ./Text/package.dhall sha256:c8bc93456397476051dc674c180ddd5db098546861c8df24bda8284511d3305e ? ./Text/package.dhall }