-
Robbert Krebbers authored
Type environments now describe alignment, this allows to: * Prove properties about alignment, for example that bit offsets of addresses are always aligned. * Support align_of expressions in the frontend.
8b7ea9be
Type environments now describe alignment, this allows to: * Prove properties about alignment, for example that bit offsets of addresses are always aligned. * Support align_of expressions in the frontend.