diff options
| author | Brian Campbell | 2018-08-02 15:58:45 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-02 18:16:55 +0100 |
| commit | 8a06df3ad1b90a355d3e5adb694002f00e67823e (patch) | |
| tree | c6d5beadc94d7695c02cc4f7d4b0af1f8deeca51 /lib | |
| parent | 5980711d118ad6d0c28644be605447c3dc82be64 (diff) | |
Fill in more Coq builtins for aarch64
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 5752e6c0..6fcbbb52 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -54,7 +54,10 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y)) }. destruct (eqdec x y); simpl; split; congruence. -Qed. +Defined. + +Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) := + Decidable_eq_from_dec String.string_dec. (* Project away range constraints in comparisons *) |