• Robbert Krebbers's avatar
    Support alignment. · 8b7ea9be
    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
numbers.v 18.4 KB