diff options
| author | Brian Campbell | 2019-06-13 18:01:24 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-06-13 18:03:07 +0100 |
| commit | 54a08099f2360372a1e94f9ed0489a1dc89351af (patch) | |
| tree | af7737dd81f753de2b6450eab23d7eff52eea919 /lib | |
| parent | d2f702da3b5cc9934f8cd3ea457f93c6ce2b6c12 (diff) | |
Coq: add eq_bit built-in
Diffstat (limited to 'lib')
| -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. |