From 8ad9b84c8570b16ef4277f19011fbd791e8e6419 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Dec 2014 18:49:19 -0800 Subject: [PATCH] feat(init): reserve notation for "not in" --- hott/init/reserved_notation.hlean | 1 + library/init/reserved_notation.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index 4f7d4651a..fa389edd8 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -73,6 +73,7 @@ reserve infixl `||`:65 /- set operations -/ reserve infix `∈`:50 +reserve infix `∉`:50 reserve infixl `∩`:70 reserve infixl `∪`:65 diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index ecc5b9208..973d6d278 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -72,6 +72,7 @@ reserve infixl `||`:65 /- set operations -/ reserve infix `∈`:50 +reserve infix `∉`:50 reserve infixl `∩`:70 reserve infixl `∪`:65