diff options
| author | Jason Gross | 2018-11-28 15:16:31 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:16:31 -0500 |
| commit | f5e3d9e29f030a86433bb2700e55c4c183593163 (patch) | |
| tree | 519a8de15016906348e69a03560c0d8393215d7e /test-suite | |
| parent | 5537151575195addd3e1e0003025384a85d957f7 (diff) | |
Byte.v: use right-associative tuples in bits
We encode the conversion to bits with little-endian right-associative
tuples to ensure that the head of the tuple (the `fst` element) is the
least significant bit. We still enforce that the ordering of bits
matches the order of the `bool`s in the `ascii` inductive type.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Search.out | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 20b154b5d0..f4544a0df3 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -46,9 +46,11 @@ eq_true_ind: eq_true_ind_r: forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true Byte.to_bits: - Byte.byte -> bool * bool * bool * bool * bool * bool * bool * bool + Byte.byte -> + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) Byte.of_bits: - bool * bool * bool * bool * bool * bool * bool * bool -> Byte.byte + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> + Byte.byte andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true @@ -57,7 +59,8 @@ BoolSpec_ind: (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b Byte.to_bits_of_bits: - forall b : bool * bool * bool * bool * bool * bool * bool * bool, + forall + b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b bool_choice: forall (S : Set) (R1 R2 : S -> Prop), |