RefMut can be considered as Sync
I figured out that RefMut could be considered as Sync even though Rust stdlib does not consider it as such.
I find this is an interesting fact, so I added it to our formalization. This is not particularly useful for writing programs, because a value of type &RefMut<T>
can be WLOG unnested to a &T
, but still this is interesting from a type system's perspective.