Advertisement
Guest User

Untitled

a guest
Jun 18th, 2019
69
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.68 KB | None | 0 0
  1. {- The intersperse function takes an element and a list and `intersperses' that element between the elements of the list. For example,
  2.  
  3. ```
  4. intersperse Natural 0 [ 1, 2, 3, 4 ] = [ 1, 0, 2, 0, 3, 0, 4 ]
  5. ```
  6. -}
  7. let List/intersperse
  8. : ∀(e : Type) → e → List e → List e
  9. = λ(e : Type)
  10. → λ(separator : e)
  11. → λ(list : List e)
  12. → let cons =
  13. λ(element : e)
  14. → λ(continue : List e → List e)
  15. → λ(step : List e)
  16. → continue
  17. ( if ./null.dhall e step
  18.  
  19. then [ element ]
  20.  
  21. else step # [ separator, element ]
  22. )
  23.  
  24. let nil = λ(x : List e) → x
  25.  
  26. in List/fold e list (List e → List e) cons nil ([] : List e)
  27.  
  28. in List/intersperse
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement