Merge pull request #2158 from david-christiansen/mrmonday-until
Put until into contrib.
commit3ac0d5a89851de1fdea4d8e6847780d931fc1124
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 19 Apr 2015, 12:44 (12 years ago)
parentbc7b1e52c0d83a
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
libs/contrib/contrib.ipkg+2−1
@@ -3,9 +3,10 @@ package contrib
33opts = "--nobasepkgs --total -i ../prelude -i ../base"
44modules = Control.Algebra,
55 Control.Isomorphism.Primitives,
6+ Control.Partial,
67 Control.WellFounded,
78 Classes.Verified,
8− Data.Fun, Data.Rel,
9+ Data.Fun, Data.Rel,
910 Data.Hash, Data.Matrix,
1011 Data.Nat,
1112 Data.ZZ, Data.Sign,