In SML and in Coq, it is possible to write a parameterised module, a functor in Standard ML parlance.
Is the form
locale second = first + assumes ... ...first.def2...
a functor in this sense?
I have read that locales are limited contrasted to Coq modules --- what is the difference in expressiveness?
I'd say the functor analogy is fine. The isar ref puts it as follows:
A locale is a functor that maps parameters (including implicit type param-eters) and a specification to a list of declarations
I have no experience with Coq, so I cannot comment on the latter. Do you happen to have a reference to said text?
Last updated: Sep 25 2021 at 08:21 UTC