Closed andrew-appel closed 3 months ago
The lemmas data_at_int_or_ptr_int and data_at_int_or_ptr_ptr in floyd/field_at.v should be generalized, so they don't require Tsh but work for any share. This is trivial to do.
data_at_int_or_ptr_int
data_at_int_or_ptr_ptr
The lemmas
data_at_int_or_ptr_intanddata_at_int_or_ptr_ptrin floyd/field_at.v should be generalized, so they don't require Tsh but work for any share. This is trivial to do.