The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 06/01/2021 17:45, jonikelee AT gmail.com wrote:
> Why not provide both?  They're both very useful for different purposes.
> Introduce the keyword "special" to distinguish when the binding is
> dynamic.

State is more expressive than reader, since you can implement the latter
with the former. So the question is rather if we want to give the full
power of state in the rebinding of global definitions. Typically,
limiting expressivity can be worthwhile for code modularity.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature