From 5721bc13a736ed9facabfeb730a29c073156a653 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Nov 2015 15:22:40 -0800
Subject: [PATCH] feat(library/init/logic): annotate logical connectives as
 [no_pattern]

---
 library/init/logic.lean | 12 +++++++++++-
 library/init/num.lean   |  9 +--------
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index a82c8ee29..bc653e9ad 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
-import init.datatypes init.reserved_notation
+import init.datatypes init.reserved_notation init.tactic
 
 definition id [reducible] [unfold_full] {A : Type} (a : A) : A :=
 a
@@ -698,6 +698,12 @@ inhabited.mk (λa, !default)
 protected definition bool.is_inhabited [instance] : inhabited bool :=
 inhabited.mk ff
 
+protected definition pos_num.is_inhabited [instance] : inhabited pos_num :=
+inhabited.mk pos_num.one
+
+protected definition num.is_inhabited [instance] : inhabited num :=
+inhabited.mk num.zero
+
 inductive nonempty [class] (A : Type) : Prop :=
 intro : A → nonempty A
 
@@ -892,6 +898,10 @@ if Hc : c then !false.rec (if_pos Hc ▸ H₂) else Hc
 theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c :=
 if Hc : c then Hc else absurd trivial (if_neg Hc ▸ H₂)
 
+-- The following symbols should not be considered in the pattern inference procedure used by
+-- heuristic instantiation.
+attribute and or not iff ite dite eq ne heq [no_pattern]
+
 -- namespace used to collect congruence rules for "contextual simplification"
 namespace contextual
   attribute if_ctx_simp_congr      [congr]
diff --git a/library/init/num.lean b/library/init/num.lean
index 80f5d5ab2..84eee1787 100644
--- a/library/init/num.lean
+++ b/library/init/num.lean
@@ -3,14 +3,10 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-
 prelude
-import init.logic init.bool
+import init.bool
 open bool
 
-definition pos_num.is_inhabited [instance] : inhabited pos_num :=
-inhabited.mk pos_num.one
-
 namespace pos_num
   protected definition mul (a b : pos_num) : pos_num :=
   pos_num.rec_on a
@@ -41,9 +37,6 @@ end pos_num
 definition pos_num_has_mul [instance] [reducible] : has_mul pos_num :=
 has_mul.mk pos_num.mul
 
-definition num.is_inhabited [instance] : inhabited num :=
-inhabited.mk num.zero
-
 namespace num
   open pos_num