diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-27 10:52:24 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-27 10:52:43 -0700 |
| commit | fb208af406edf5ae94f9e2e08fb2119ba1cc8d62 (patch) | |
| tree | cfb13392a7cfe547063e92c566c0d815b938ad02 /src/Algebra.v | |
| parent | 1da660b30f87a161f866deb44717d0ba5c78cd9d (diff) | |
Add global notation for eq_dec
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index b1fdc69a3..ae12f3a7e 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -13,6 +13,7 @@ Notation is_eq_dec := (DecidableRel _) (only parsing). Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) (at level 10, T at level 8, R at level 8, only parsing). Notation eq_dec x y := (@dec (_ x y) _) (only parsing). +Notation "x =? y" := (eq_dec x y) : type_scope. Section Algebra. Context {T:Type} {eq:T->T->Prop}. |