diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 5bc630e5..afa22856 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -81,6 +81,11 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> destruct (eqdec x y); simpl; split; congruence. Defined. +Instance Decidable_eq_unit : forall (x y : unit), Decidable (x = y) := + { Decidable_witness := true }. +destruct x, y; split; auto. +Defined. + Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) := Decidable_eq_from_dec String.string_dec. |