GitLab

Currently the generated unfolding lemmas (e.g. https://gitlab.mpi-sws.org/iris/refinedc/-/blob/a08924ffbba96010976fa2e7910822799cb072a2/theories/examples/tutorial/misc_spec.v#L42) are available to both the implementation and the clients of a type. Arguably, the client should never unfold the definition and thus the unfolding lemmas should not be available for the client. Allowing the unfolding can lead to clients relying on internals of types which should be abstract and to confusing errors (talking about the unfolded type instead of the folded type).

Idea: Add a Unfoldable ty type class parameter to the unfolding lemmas such that they only apply if an instance for this type class exists. Then the implementation can provide such a type class instance while the client code does not. Maybe the type class instance can be generated from an annotation in the source code.