fix(proof-libs/f*): f_deref: make it a typeclass

cryspen · Jul 10, 2024 · e7b724a · e7b724a
1 parent 9137617
commit e7b724a
Showing 1 changed file with 10 additions and 1 deletion.
diff --git a/proof-libs/fstar/core/Core.Ops.Deref.fst b/proof-libs/fstar/core/Core.Ops.Deref.fst
@@ -1,3 +1,12 @@
 module Core.Ops.Deref
 
-let f_deref = id
+class t_Deref (t_Self: Type0) = {
+   f_Target: Type0;
+   f_deref: t_Self -> f_Target;
+}
+
+unfold
+instance identity_Deref t_Self: t_Deref t_Self = {
+  f_Target = t_Self;
+  f_deref = (fun x -> x);
+}