RecordsNotModules

Pierre-Marie Pédrot edited this page Feb 27, 2018 · 9 revisions

The main bulk of the modules and functor system can be replaced by dependent record types and functions instead. Because of this, there is little reason to use modules other than to provide namespace support. In fact, there are good reasons not to use modules. Most importantly, module parameters cannot be instantiated with variables. See Carlos Simpson's post to coq-club.

See Coq's standard library for examples of how to do this.

Note that the TypeClasses feature uses dependent records internally to provide modularity.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.