• Robbert Krebbers's avatar
    Stronger allocation updates for gset. · fcc1c439
    Robbert Krebbers authored
    The new updates allow allocation fresh elements satisfying an arbitrary
    proposition (for example, being even) instead of just not being in a given
    finite set.
    
    TODO: maybe also do this for finite maps (gmaps).
    fcc1c439
gset.v 4.69 KB