diff options
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index bd22371a..e152fb67 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -385,6 +385,7 @@ Qed. Inductive bitU := B0 | B1 | BU. Scheme Equality for bitU. +Definition eq_bit := bitU_beq. Instance Decidable_eq_bit : forall (x y : bitU), Decidable (x = y) := Decidable_eq_from_dec bitU_eq_dec. |