Stream: Beginner Questions

Topic: Locales as modules

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

                 ...first.def2...

a functor in this sense?

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

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: Apr 20 2024 at 04:19 UTC