From 712d6726e4020dbb37ddd6e9ccda124a9efe741d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Feb 2022 17:11:07 -0800
Subject: [PATCH] feat: rename tactic `byCases` => `by_cases`

---
 RELEASES.md                     | 2 ++
 src/Init/Classical.lean         | 2 +-
 tests/lean/run/ac_expr.lean     | 4 ++--
 tests/lean/run/specialize2.lean | 2 +-
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/RELEASES.md b/RELEASES.md
index f0eff2616f..78a45b0faa 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -27,3 +27,5 @@ theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)]
 * [Relax auto-implicit restrictions](https://github.com/leanprover/lean4/pull/1011). The command `set_option relaxedAutoImplicit false` disables the relaxations.
 
 * `contradiction` tactic now closes the goal if there is a `False.elim` application in the target.
+
+* Renamed tatic `byCases` => `by_cases` (motivation: enforcing naming convention).
diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 3e63cdfdec..95262b0173 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -125,7 +125,7 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 
-macro "byCases" h:ident ":" e:term : tactic =>
+macro "by_cases" h:ident ":" e:term : tactic =>
   `(cases em $e:term with
     | inl $h:ident => _
     | inr $h:ident => _)
diff --git a/tests/lean/run/ac_expr.lean b/tests/lean/run/ac_expr.lean
index ce702ccf28..ee8ce1c51c 100644
--- a/tests/lean/run/ac_expr.lean
+++ b/tests/lean/run/ac_expr.lean
@@ -105,7 +105,7 @@ where
       | var i =>
         cases a with
         | var j =>
-          byCases h : i > j
+          by_cases h : i > j
           focus
             simp [sort.swap, h]
             match h:sort.swap (var j) b with
@@ -123,7 +123,7 @@ where
     | var j =>
       cases e₁ with
       | var i =>
-        byCases h : i > j
+        by_cases h : i > j
         focus simp [sort.swap, h, denote, Context.comm]
         focus simp [sort.swap, h]
       | _ => rfl
diff --git a/tests/lean/run/specialize2.lean b/tests/lean/run/specialize2.lean
index 82d5fc0927..8024199996 100644
--- a/tests/lean/run/specialize2.lean
+++ b/tests/lean/run/specialize2.lean
@@ -1,7 +1,7 @@
 example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by
   apply Iff.intro
   . intro h
-    byCases hp:p <;> byCases hq:q
+    by_cases hp:p <;> by_cases hq:q
     . specialize h hp hq; contradiction
     . exact Or.inr hq
     . exact Or.inl hp