diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 15:44:20 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 15:44:20 +0200 |
| commit | 5ffa8534d09272e5f44c51193e74cffdbc2b043c (patch) | |
| tree | c391ce9fa363db667a36775c8cf56a6e6f484ed0 /lib | |
| parent | bd4fbff2badea3922bf0e144777ae8ecfdc30e74 (diff) | |
| download | compcert-kvx-5ffa8534d09272e5f44c51193e74cffdbc2b043c.tar.gz compcert-kvx-5ffa8534d09272e5f44c51193e74cffdbc2b043c.zip | |
Icond
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Integers.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 9c6fcf1d..08a416c1 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -29,6 +29,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne |