3ac0d5a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2158 from david-christiansen/mrmonday-until

3ac0d5aDavid Christiansen12 years ago

libs/contrib/Control/Partial.idrnew file+14

@@ -0,0 +1,14 @@

1+||| Control structures that are fundamentally partial

2+module Control.Partial

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

3opts = "--nobasepkgs --total -i ../prelude -i ../base"

4modules = Control.Algebra,

5 Control.Isomorphism.Primitives,

6+ Control.Partial,

6 Control.WellFounded,

7 Control.WellFounded,

7 Classes.Verified,

8 Classes.Verified,

8− Data.Fun, Data.Rel,

9+ Data.Fun, Data.Rel,

9 Data.Hash, Data.Matrix,

10 Data.Hash, Data.Matrix,

10 Data.Nat,

11 Data.Nat,

11 Data.ZZ, Data.Sign,

12 Data.ZZ, Data.Sign,