edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-01 17:23:23 +03:00
Code Issues Projects Releases Wiki Activity

Add replicate to base/Data.List.

Browse Source
This commit is contained in:
Michael Morgan 2019-10-29 16:06:48 -07:00
parent ab98b4d3c9
commit 9190ccf883
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libs/base/Data/List.idr
View File

@ -121,6 +121,13 @@ public export
reverse : List a -> List a
reverse = reverseOnto []
||| Construct a list with `n` copies of `x`.
||| @ n how many copies
||| @ x the element to replicate
public export
replicate : (n : Nat) -> (x : a) -> List a
replicate Z _ = []
replicate (S n) x = x :: replicate n x
||| Compute the intersect of two lists by user-supplied equality predicate.
export