29 May
2026
29 May
'26
1:37 a.m.
True! Thanks—Michael
From: Makarius makarius@sketis.net Date: Thursday, 28 May 2026 at 19:27 To: Michael Norrish Michael.Norrish@anu.edu.au; polyml@lists.polyml.org polyml@lists.polyml.org Subject: Re: [Polyml] Re: Mutex as eqtype?
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