for package:Agda
The true pure
for loop.
for is a misnomer, it should
be
forA.
Get content of
FOREIGN GHC pragmas, sorted by
KindOfForeignCode: file header pragmas, import statements,
rest.
Compute a position position prefix.
Depending on the error to be printed, it will
- either give the name of the libraries file and a line
inside it,
- or give the name of the .agda-lib file.
Build a forall pi (forall x y z -> ...)
Try to enforce a set of variables not occurring in a given type.
Returns a possibly reduced version of the type and for each of the
given variables whether it is either not free, or maybe free depending
on some metavariables.
Runs the given computation in a separate thread, with a copy of
the current state and environment.
Note that Agda sometimes uses actual, mutable state. If the
computation given to forkTCM tries to modify this
state, then bad things can happen, because accesses are not mutually
exclusive. The forkTCM function has been added mainly to
allow the thread to read (a snapshot of) the current state in a
convenient way.
Note also that exceptions which are raised in the thread are not
propagated to the parent, so the thread should not do anything
important.
Eta expand a record regardless of whether it's an eta-record or not.
Ensure that the type is a sort. If it is not directly a sort, compare
it to a
newSortMetaBelowInf.
Version of
mapMaybe with different argument ordering.
forM is
mapM with its arguments flipped. For a version
that ignores the results see
forM_.
Generalized version of for_ :: Applicative m => [a] -> (a
-> m ()) -> m ()
forM_ is
mapM_ with its arguments flipped. For a version
that doesn't ignore the results see
forM.
forM_ is just like
for_, but specialised to monadic
actions.