Merge branch 'until' of https://github.com/mrmonday/Idris-dev into mrmonday-until
commit6d747308b0cc6aa270c3c75d7d143e0ff3da97b2
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateSat 18 Apr 2015, 18:17 (12 years ago)
parent4f4c993663b670
libs/contrib/Control/Partial.idrnew file+14
@@ -0,0 +1,14 @@
1+||| Control structures that are fundamentally partial
2+module Control.Partial
3+
4+
5+||| Repeatedly apply `f` to `v` until `p` is `True`.
6+|||
7+||| @ p the predicate to wait for
8+||| @ f the function to repeatedly apply
9+||| @ v the starting value
10+partial
11+until : (p : a -> Bool) -> (f : a -> a) -> (v : a) -> a
12+until p f v with (p v)
13+ | False = until p f (f v)
14+ | True = v