rename ac_nf! to ac_nf'

src/Lean/Meta/Tactic/AC/Sharing.lean

@@ -251,16 +251,16 @@ def acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := do
     let (res, _) ← Simp.main tgt simpCtx (methods := { post := canonicalizeWithSharing })
     return (← applySimpResultToLocalDecl goal fvarId res false).map (·.snd)
 
-/-- Implementation of the `ac_nf!` tactic when operating on the main goal. -/
+/-- Implementation of the `ac_nf'` tactic when operating on the main goal. -/
 def acNfTargetTactic : TacticM Unit :=
   liftMetaTactic1 fun goal => rewriteUnnormalizedWithSharing goal
 
-/-- Implementation of the `ac_nf!` tactic when operating on a hypothesis. -/
+/-- Implementation of the `ac_nf'` tactic when operating on a hypothesis. -/
 def acNfHypTactic (fvarId : FVarId) : TacticM Unit :=
   liftMetaTactic1 fun goal => acNfHypMeta goal fvarId
 
 open Lean.Parser.Tactic (location) in
-elab "ac_nf!" loc?:(location)? : tactic => do
+elab "ac_nf'" loc?:(location)? : tactic => do
   let loc := match loc? with
   | some loc => expandLocation loc
   | none => Location.targets #[] true

tests/lean/run/ac_nf.lean

@@ -8,27 +8,27 @@ open Lean
 
 theorem mul_mul_eq_mul_mul (x₁ x₂ y₁ y₂ z : BitVec 4) (h₁ : x₁ = x₂) (h₂ : y₁ = y₂) :
     x₁ * (y₁ * z) = x₂ * (y₂ * z) := by
-  ac_nf!
+  ac_nf'
   show z * (x₁ * y₁) = z * (x₂ * y₂)
   sorry
 
 -- This theorem is short-circuited and scales to standard bitwidths.
 theorem mul_eq_mul_eq_right (x y z : BitVec 64) (h : x = y) :
     x * z = y * z := by
-  ac_nf!
+  ac_nf'
   show z * x = z * y
   sorry
 
 -- This theorem is short-circuited and scales to standard bitwidths.
 theorem mul_eq_mul_eq_left (x y z : BitVec 64) (h : x = y) :
     z * x = z * y := by
-  ac_nf!
+  ac_nf'
   show z * x = z * y
   sorry
 
 theorem short_circuit_triple_mul (x x_1 x_2 : BitVec 32) (h : ¬x_2 &&& 4096#32 == 0#32) :
     (x_1 ||| 4096#32) * x * (x_1 ||| 4096#32) = (x_1 ||| x_2 &&& 4096#32) * x * (x_1 ||| 4096#32) := by
-  ac_nf!
+  ac_nf'
   sorry
 
 /-! ### Scaling Test -/
@@ -44,7 +44,7 @@ local macro "repeat_add" n:num "with" x:term  : term =>
   go n.getNat
 
 /-
-This test showcases that the runtime of `ac_nf!` is not a bottleneck:
+This test showcases that the runtime of `ac_nf'` is not a bottleneck:
 * The current example runs in about 250ms with a disabled kernel, or ~5 seconds with,
     showing that the tactic runtime is tiny compared to the proof-checking time, and
 * Putting in 125 for the repitition amount wil give a `maximum recursion depth has been reached`
@@ -53,4 +53,4 @@ This test showcases that the runtime of `ac_nf!` is not a bottleneck:
 set_option debug.skipKernelTC true in
 example (x y : BitVec 64) :
     (repeat_add 124 with x + y) = (repeat_add 124 with x) + (repeat_add 124 with y) := by
-  ac_nf!; rfl
+  ac_nf'; rfl