diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-13 14:46:33 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-13 15:37:16 -0500 |
| commit | b2a1a0c0360ae4cb35f0bcfb34bb86b4734c4800 (patch) | |
| tree | 1a1c419a4493b4e046f0fccc475ecaf008a5ede1 /src/Compilers | |
| parent | a26f3c7a9c8ad648a4706d1dae374f739f7c73c1 (diff) | |
Add some convenience notations in Z.Syntax.Equality
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/Syntax/Equality.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Equality.v b/src/Compilers/Z/Syntax/Equality.v index caa209e52..0ff0fabf0 100644 --- a/src/Compilers/Z/Syntax/Equality.v +++ b/src/Compilers/Z/Syntax/Equality.v @@ -16,6 +16,12 @@ Global Instance dec_eq_base_type : DecidableRel (@eq base_type) Global Instance dec_eq_flat_type : DecidableRel (@eq (flat_type base_type)) := _. Global Instance dec_eq_type : DecidableRel (@eq (type base_type)) := _. +Notation base_type_dec_bl := internal_base_type_dec_bl. +Notation base_type_dec_lb := internal_base_type_dec_lb. +Notation flat_type_beq := (@flat_type_beq base_type base_type_beq). +Notation flat_type_dec_bl := (@flat_type_dec_bl base_type base_type_beq base_type_dec_bl). +Notation flat_type_dec_lb := (@flat_type_dec_lb base_type base_type_beq base_type_dec_lb). + Definition base_type_eq_semidec_transparent (t1 t2 : base_type) : option (t1 = t2) := match base_type_eq_dec t1 t2 with |