WF

theories/typing/lib/mutex/mutex.v

@@ -83,4 +83,8 @@ Section mutex.
     iExists _, _. iSplit; first by iApply shr_bor_shorten.
     iApply lft_incl_trans; done.
   Qed.
+
+  Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
 End mutex.

theories/typing/lib/mutex/mutexguard.v

@@ -75,4 +75,8 @@ Section mguard.
       iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
       iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
   Qed.
+
+  Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+
 End mguard.

theories/typing/lib/rwlock/rwlock.v

@@ -149,7 +149,7 @@ Section rwlock.
     iExists _, _. iFrame. iApply lft_incl_trans; auto.
   Qed.
 
-  Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
+  Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
   Global Instance rwlock_type_ne : TypeNonExpansive rwlock.