The documentation on modules is incomplete.
https://agda.readthedocs.io/en/v2.6.4.1/language/module-system.html
It should be edited so that "Module application" and "Anonymous modules" are nonempty.
@plt-amy As the 1lab makes frequent use of anonymous modules, maybe you would be interested in contributing a paragraph or two here to help contributors understand the purpose of this design pattern? It is not immediately obvious to an outsider what the usefulness is of a definition which cannot be referred to.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4