From dfaeb475cc0bd4c8953502a33742e269eb1986dd Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 18 Apr 2015 13:41:58 -0400 Subject: [PATCH] feat(library/init/reserved_notation.lean): add equiv relation symbol --- library/init/reserved_notation.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index c511cb0e63..010ab1c9b6 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -46,6 +46,7 @@ reserve infix `=`:50 reserve infix `≠`:50 reserve infix `≈`:50 reserve infix `∼`:50 +reserve infix `≡`:50 reserve infixr `∘`:60 -- input with \comp reserve postfix `⁻¹`:std.prec.max_plus -- input with \sy or \-1 or \inv