Stream: Beginner Questions

Topic: Locales as modules

view this post on Zulip Gergely Buday (Aug 12 2020 at 07:29):

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 ...


a functor in this sense?

I have read that locales are limited contrasted to Coq modules --- what is the difference in expressiveness?

view this post on Zulip Kevin Kappelmann (Aug 13 2020 at 09:09):

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: Aug 10 2022 at 19:17 UTC