notice some type properties that still need proving

theories/typing/lib/mutex/mutex.v

@@ -87,6 +87,8 @@ Section mutex.
   Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) :=
     { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
 
+  (* TODO: Non-expansiveness, compat with eqtype, Send+Sync if ty is Send. *)
+
 End mutex.
 
 Section code.

theories/typing/lib/mutex/mutexguard.v

@@ -79,6 +79,9 @@ Section mguard.
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
     { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
 
+  (* TODO: Contractivity, compat with lft_incl and eqtype.
+     MutexGuard is Sync if T is Send. *)
+
 End mguard.
 
 Section code.

theories/typing/lib/rwlock/rwlockreadguard.v

@@ -112,6 +112,8 @@ Section rwlockreadguard.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
   Proof. intros. by eapply rwlockreadguard_proper. Qed.
+
+  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
 End rwlockreadguard.
 
 Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.

theories/typing/lib/rwlock/rwlockwriteguard.v

@@ -115,6 +115,8 @@ Section rwlockwriteguard.
     lctx_lft_eq E L α1 α2 → eqtype E L ty1 ty2 →
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
+
+  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.