28 May
2026
28 May
'26
10:26 a.m.
On 28/05/2026 01:31, Michael Norrish wrote:
The reason I ask is because I would like to replace a standard ref with an Isabelle-derived Sref.t type in a larger composite type, and I can’t make the Sref an equality type unless the Mutex is one too.
You could wrap another ref type constructor around the mutex, and keep that private to the new type.
Makarius