Executes a monadic action on all the numbers less than some bound, in decreasing order.
Example:
#eval Nat.forRevM 5 fun i _ => IO.println i
4
3
2
1
0
Equations
Instances For
Iterates the application of a monadic function f
to a starting value init
, n
times. At each
step, f
is applied to the current value and to the next natural number less than n
, in
increasing order.
Equations
Instances For
Iterates the application of a monadic function f
to a starting value init
, n
times. At each
step, f
is applied to the current value and to the next natural number less than n
, in
decreasing order.
Equations
Instances For
Checks whether the monadic predicate p
returns true
for all numbers less that the given bound.
Numbers are checked in increasing order until p
returns false, after which no further are checked.
Equations
Instances For
Checks whether there is some number less that the given bound for which the monadic predicate p
returns true
. Numbers are checked in increasing order until p
returns true, after which
no further are checked.