Skip to content
This repository has been archived by the owner on Dec 30, 2018. It is now read-only.

Use new Some and None constructors #9

Merged
merged 1 commit into from Sep 10, 2018
Merged

Use new Some and None constructors #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
16 changes: 8 additions & 8 deletions Bool/package.dhall
View file
Open in desktop
@@ -1,17 +1,17 @@
{ and =
./and
./and
, build =
./build
./build
, even =
./even
./even
, fold =
./fold
./fold
, not =
./not
./not
, odd =
./odd
./odd
, or =
./or
./or
, show =
./show
./show
}
2 changes: 1 addition & 1 deletion Double/package.dhall
View file
Open in desktop
@@ -1 +1 @@
{ show = ./show }
{ show = ./show }
2 changes: 1 addition & 1 deletion Integer/package.dhall
View file
Open in desktop
@@ -1 +1 @@
{ show = ./show }
{ show = ./show }
2 changes: 1 addition & 1 deletion JSON/Tagged
View file
Open in desktop
Expand Up @@ -64,6 +64,6 @@ in { provisioners =
-}
let Tagged
: Type → Type
= λ(a : Type) → { field : Text, nesting : ./Nesting , contents : a }
= λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a }

in Tagged
4 changes: 1 addition & 3 deletions JSON/package.dhall
View file
Open in desktop
@@ -1,3 +1 @@
{ keyText = ./keyText
, keyValue = ./keyValue
}
{ keyText = ./keyText, keyValue = ./keyValue }
4 changes: 2 additions & 2 deletions List/head
View file
Open in desktop
Expand Up @@ -4,9 +4,9 @@ Retrieve the first element of the list
Examples:

```
./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural
./head Natural [ 0, 1, 2 ] = Some 0

./head Natural ([] : List Natural) = [] : Optional Natural
./head Natural ([] : List Natural) = None Natural
```
-}
let head : ∀(a : Type) → List a → Optional a = List/head in head
4 changes: 2 additions & 2 deletions List/last
View file
Open in desktop
Expand Up @@ -4,9 +4,9 @@ Retrieve the last element of the list
Examples:

```
./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural
./last Natural [ 0, 1, 2 ] = Some 2

./last Natural ([] : List Natural) = [] : Optional Natural
./last Natural ([] : List Natural) = None Natural
```
-}
let last : ∀(a : Type) → List a → Optional a = List/last in last
38 changes: 19 additions & 19 deletions List/package.dhall
View file
Open in desktop
@@ -1,39 +1,39 @@
{ all =
./all
./all
, any =
./any
./any
, build =
./build
./build
, concat =
./concat
./concat
, concatMap =
./concatMap
./concatMap
, filter =
./filter
./filter
, fold =
./fold
./fold
, generate =
./generate
./generate
, head =
./head
./head
, indexed =
./indexed
./indexed
, iterate =
./iterate
./iterate
, last =
./last
./last
, length =
./length
./length
, map =
./map
./map
, null =
./null
./null
, replicate =
./replicate
./replicate
, reverse =
./reverse
./reverse
, shifted =
./shifted
./shifted
, unzip =
./unzip
./unzip
}
11 changes: 7 additions & 4 deletions List/shifted
View file
Open in desktop
Expand Up @@ -58,8 +58,9 @@ Bool
{ index : Natural, value : a }
kvs

in { count = y.count + length
, diff =
in { count =
y.count + length
, diff =
λ(n : Natural)
→ List/fold
{ index : Natural, value : a }
Expand All @@ -70,8 +71,10 @@ Bool
)
→ λ(z : list)
→ let kvNew =
{ index = kvOld.index + n
, value = kvOld.value
{ index =
kvOld.index + n
, value =
kvOld.value
}

in cons kvNew z
Expand Down
20 changes: 10 additions & 10 deletions Natural/package.dhall
View file
Open in desktop
@@ -1,21 +1,21 @@
{ build =
./build
./build
, enumerate =
./enumerate
./enumerate
, even =
./even
./even
, fold =
./fold
./fold
, isZero =
./isZero
./isZero
, odd =
./odd
./odd
, product =
./product
./product
, sum =
./sum
./sum
, show =
./show
./show
, toInteger =
./toInteger
./toInteger
}
13 changes: 0 additions & 13 deletions Optional/None
View file
Open in desktop

This file was deleted.

13 changes: 0 additions & 13 deletions Optional/Some
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions Optional/all
View file
Open in desktop
Expand Up @@ -5,9 +5,9 @@ and `True` otherwise:
Examples:

```
./all Natural Natural/even ([ 3 ] : Optional Natural) = False
./all Natural Natural/even (Some 3) = False

./all Natural Natural/even ([] : Optional Natural) = True
./all Natural Natural/even (None Natural) = True
```
-}
let all
Expand Down
4 changes: 2 additions & 2 deletions Optional/any
View file
Open in desktop
Expand Up @@ -5,9 +5,9 @@ Returns `True` if the supplied function returns `True` for a present element and
Examples:

```
./any Natural Natural/even ([ 2 ] : Optional Natural) = True
./any Natural Natural/even (Some 2) = True

./any Natural Natural/even ([] : Optional Natural) = False
./any Natural Natural/even (None Natural) = False
```
-}
let any
Expand Down
20 changes: 10 additions & 10 deletions Optional/build
View file
Open in desktop
Expand Up @@ -7,27 +7,27 @@ Examples:
./build
Natural
( λ(optional : Type)
→ λ(just : Natural → optional)
→ λ(nothing : optional)
→ just 1
→ λ(some : Natural → optional)
→ λ(none : optional)
→ some 1
)
= [ 1 ] : Optional Natural
= Some 1

./build
Natural
( λ(optional : Type)
→ λ(just : Natural → optional)
→ λ(nothing : optional)
→ nothing
→ λ(some : Natural → optional)
→ λ(none : optional)
→ none
)
= [] : Optional Natural
= None Natural
```
-}
let build
: ∀(a : Type)
→ ( ∀(optional : Type)
→ ∀(just : a → optional)
→ ∀(nothing : optional)
→ ∀(some : a → optional)
→ ∀(none : optional)
→ optional
)
→ Optional a
Expand Down
14 changes: 7 additions & 7 deletions Optional/concat
View file
Open in desktop
Expand Up @@ -4,14 +4,14 @@ Flatten two `Optional` layers into a single `Optional` layer
Examples:

```
./concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural))
= [ 1 ] : Optional Natural
./concat Natural (Some (Some 1))
= Some 1

./concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural))
= [] : Optional Natural
./concat Natural (Some (None Natural))
= None Natural

./concat Natural ([] : Optional (Optional Natural))
= [] : Optional Natural
./concat Natural (None (Optional Natural))
= None Natural
```
-}
let concat
Expand All @@ -23,6 +23,6 @@ Examples:
x
(Optional a)
(λ(y : Optional a) → y)
([] : Optional a)
(None a)

in concat
16 changes: 8 additions & 8 deletions Optional/filter
View file
Open in desktop
Expand Up @@ -4,11 +4,11 @@ Only keep an `Optional` element if the supplied function returns `True`
Examples:

```
./filter Natural Natural/even ([ 2 ] : Optional Natural)
= [ 2 ] : Optional Natural
./filter Natural Natural/even (Some 2)
= Some 2

./filter Natural Natural/odd ([ 2 ] : Optional Natural)
= [] : Optional Natural
./filter Natural Natural/odd (Some 2)
= None Natural
```
-}
let filter
Expand All @@ -19,14 +19,14 @@ Examples:
→ Optional/build
a
( λ(optional : Type)
→ λ(just : a → optional)
→ λ(nil : optional)
→ λ(some : a → optional)
→ λ(none : optional)
→ Optional/fold
a
xs
optional
(λ(x : a) → if f x then just x else nil)
nil
(λ(x : a) → if f x then some x else none)
none
)

in filter
8 changes: 4 additions & 4 deletions Optional/fold
View file
Open in desktop
Expand Up @@ -4,17 +4,17 @@
Examples:

```
./fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 2
./fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 = 2

./fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 0
./fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 = 0
```
-}
let fold
: ∀(a : Type)
→ Optional a
→ ∀(optional : Type)
→ ∀(just : a → optional)
→ ∀(nothing : optional)
→ ∀(some : a → optional)
→ ∀(none : optional)
→ optional
= Optional/fold

Expand Down
20 changes: 5 additions & 15 deletions Optional/head
View file
Open in desktop
Expand Up @@ -4,21 +4,11 @@ Returns the first non-empty `Optional` value in a `List`
Examples:

```
./head
Natural
[ [ ] : Optional Natural
, [ 1 ] : Optional Natural
, [ 2 ] : Optional Natural
]
= [ 1 ] : Optional Natural
./head Natural [ None Natural, Some 1, Some 2 ] = Some 1

./head
Natural
[ [] : Optional Natural, [] : Optional Natural ]
= [] : Optional Natural
./head Natural [ None Natural, None Natural ] = None Natural

./head Natural ([] : List (Optional Natural))
= [] : Optional Natural
./head Natural ([] : List (Optional Natural)) = None Natural
```
-}
let head
Expand All @@ -31,8 +21,8 @@ Natural
(Optional a)
( λ(l : Optional a)
→ λ(r : Optional a)
→ Optional/fold a l (Optional a) (λ(x : a) → [ x ] : Optional a) r
→ Optional/fold a l (Optional a) (λ(x : a) → Some x) r
)
([] : Optional a)
(None a)

in head