move-requires.py
Moves all dependency loading statements to the top of source files.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
minimize-requires.py github.com
Removes loading of unused dependencies.
-
inline-imports.py github.com
Creates stand-alone source files from developments by inlining the loading of all dependencies.
-
absolutize-imports.py github.com
Processes source files to make loading of dependencies robust against shadowing of file names.
-
Move standard library github.com
Utilities intended (but not required) to be used in every platform running Move. From the Move repo.
-
move-vernaculars.py github.com
Lifts many vernacular commands and inner lemmas out of proof script blocks.
-
Move nursery github.com
Experimental modules that may eventually be promoted into the standard library. From the Move repo.
Coq › Projects > Tools: “Moves all dependency loading statements to the top of source files.”