packages feed

dhall-1.8.0: Prelude/Optional/toList

{-
Convert an `Optional` value into the equivalent `List`

Examples:

```
./toList Integer ([ 1 ] : Optional Integer) = [ 1 ]

./toList Integer ([] : Optional Integer) = [] : List Integer
```
-}
    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