@@ -0,0 +1,14 @@
1+||| Control structures that are fundamentally partial
5+||| Repeatedly apply `f` to `v` until `p` is `True`.
7+||| @ p the predicate to wait for
8+||| @ f the function to repeatedly apply
9+||| @ v the starting value
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)