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

                 ...first.def2...

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: Sep 25 2021 at 08:21 UTC