Skip to content
Snippets Groups Projects
Commit c88d6dd1 authored by Ralf Jung's avatar Ralf Jung
Browse files

TODO comments

parent e79c148f
No related branches found
No related tags found
No related merge requests found
Pipeline #
...@@ -267,7 +267,5 @@ Section code. ...@@ -267,7 +267,5 @@ Section code.
iApply type_jump; solve_typing. iApply type_jump; solve_typing.
Qed. Qed.
(* TODO: (* TODO: Should we do try_lock? *)
Should we do try_lock?
*)
End code. End code.
...@@ -116,7 +116,7 @@ Section rwlockwriteguard. ...@@ -116,7 +116,7 @@ Section rwlockwriteguard.
eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2). eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
Proof. intros. by eapply rwlockwriteguard_proper. Qed. Proof. intros. by eapply rwlockwriteguard_proper. Qed.
(* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *) (* TODO: In Rust, the write guard is Sync if ty is Send+Sync. *)
End rwlockwriteguard. End rwlockwriteguard.
Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing. Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment