Closed andrew-appel closed 10 months ago
In the lemma field_compatible0_Tarray_offset, the premise naturally_aligned t is totally unnecessary, it's not even used in the proof. And it's harmful, because it prevents this lemma from being use on arrays of int_or_ptr_type.
field_compatible0_Tarray_offset
naturally_aligned t
In the lemma
field_compatible0_Tarray_offset, the premisenaturally_aligned tis totally unnecessary, it's not even used in the proof. And it's harmful, because it prevents this lemma from being use on arrays of int_or_ptr_type.