From 08174f904be40b279cae9629c9ebfeabaabcbe37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jul 2014 12:01:09 -0700 Subject: [PATCH] feat(library/standard/logic): mark 'not equal' as an abbreviation Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 9678ffbd4b..bb8e43e2b8 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -160,7 +160,7 @@ theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c := assume Ha, H2 (H1 ◂ Ha) -definition ne {A : Type} (a b : A) := ¬(a = b) +definition ne [inline] {A : Type} (a b : A) := ¬(a = b) infix `≠`:50 := ne theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b