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