• Robbert Krebbers's avatar
    Support sequence point, add permissions, and update prelude. · 415a4f1c
    Robbert Krebbers authored
    Both the operational and axiomatic semantics are extended with sequence points
    and a permission system based on fractional permissions. In order to achieve
    this, the memory model has been completely revised, and is now built on top
    of an abstract interface for permissions.
    
    Apart from these changed, the library on lists and sets has been heavily
    extended, and minor changed have been made to other parts of the prelude.
    415a4f1c
listset_nodup.v 3.79 KB