iterate -is:exact -package:ghc-lib-parser package:Agda
iterate f x produces the infinite sequence of repeated
applications of
f to
x.
iterate f x = x :| [f x, f (f x), ..]
Iterate solver until no more metas can be solved.
This might trigger a (wanted) error on the second iteration (see Issue
2096) which would otherwise go unnoticed.
iterate' n f x applies
f to
x
n times and returns the result.
The applications are calculated strictly.
Iteration to fixed-point.
iterateUntil r f a0 iterates endofunction f,
starting with a0, until r relates its result to its
input, i.e., f a r a.
This is the generic pattern behind saturation algorithms.
If f is monotone with regard to r, meaning a
r b implies f a r f b, and
f-chains starting with a0 are finite then iteration
is guaranteed to terminate.
A typical instance will work on sets, and r could be set
inclusion, and a0 the empty set, and f the step
function of a saturation algorithm.
Should code points that are not supported by the locale be
transliterated?
Preprocessors for literate code formats.
Blanks the non-code parts of a given file, preserving positions of
characters corresponding to code. This way, there is a direct
correspondence between source positions and positions in the processed
result.
Short list of extensions for literate Agda files. For display
purposes.
Preprocessor for Markdown.
Preprocessor for Org mode documents.
List of valid extensions for literate Agda files, and their
corresponding preprocessors.
If you add new extensions, remember to update test/Utils.hs so that
test cases ending in the new extensions are found.
Preprocessor for reStructuredText.
Preprocessor for literate TeX.