FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
1 stars 4 forks source link

Mutex guard based Mutex API #62

Closed aseemr closed 3 weeks ago

aseemr commented 3 weeks ago

This PR tweaks the Mutex API to provide a mutex guard upon locking. Mutex guard is a ref-like type that provides read, write, replace, and a pts_to predicate. The change is quite superficial and is only intended to simplify Rust extraction.