diff options
| author | Jason Gross | 2018-11-28 14:59:20 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:01:17 -0500 |
| commit | bc6affea2270b1182181c42f3c3f06360bf216e6 (patch) | |
| tree | 5722e4ac6579f869141f3d2e5f41672899ff6ec7 /plugins/syntax/string_notation.ml | |
| parent | f7992de2dc4ce0091197b9476779fc120a2fd9ec (diff) | |
Proofs to ensure that conversions round-trip
We already have roundtrip proofs for byte<->nat, byte<->N, byte<->ascii,
N<->nat, ascii<->N, ascii<->nat, and this commit shows that all
roundtrips involving byte commute appropriately. This ensures, e.g.,
that we don't mess up and reverse the bits in conversion between byte
and ascii.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions