dzen-dhall-1.0.0: dhall/utils/intersperse.dhall

{- The intersperse function takes an element and a list and `intersperses' that element between the elements of the list. For example,

```
intersperse Natural 0 [ 1, 2, 3, 4 ] = [ 1, 0, 2, 0, 3, 0, 4 ]
```
-}
let List/null = ../prelude/List/null

let List/intersperse
	: ∀(e : Type) → e → List e → List e
	=   λ(e : Type)
	  → λ(separator : e)
	  → λ(list : List e)
	  → let cons =
				λ(element : e)
			  → λ(continue : List e → List e)
			  → λ(step : List e)
			  → continue
				(       if List/null e step

				  then  [ element ]

				  else  step # [ separator, element ]
				)

		let nil = λ(x : List e) → x

		in  List/fold e list (List e → List e) cons nil ([] : List e)

in  List/intersperse