feat(library/init/logic): annotate logical connectives as [no_pattern]

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]

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