From e1c176543a735d355de4befe6f013e52c73e61bb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 20 Feb 2024 05:53:24 -0800
Subject: [PATCH] feat: add command `norm_cast_add_elim`

---
 src/Init/Tactics.lean              | 5 +++++
 src/Lean/Elab/Tactic/NormCast.lean | 8 ++++++++
 2 files changed, 13 insertions(+)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index c757cd7b07..cbaa1a86fd 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1156,6 +1156,11 @@ end
 syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
+/--
+`norm_cast_add_elim foo` registers `foo` as an elim-lemma in `norm_cast`.
+-/
+syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
+
 end Tactic
 
 namespace Attr
diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean
index ff5fa962de..1a63c52d99 100644
--- a/src/Lean/Elab/Tactic/NormCast.lean
+++ b/src/Lean/Elab/Tactic/NormCast.lean
@@ -262,4 +262,12 @@ def evalPushCast : Tactic := fun stx => do
   dischargeWrapper.with fun discharge? =>
     discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
 
+open Command in
+@[builtin_command_elab Parser.Tactic.normCastAddElim] def elabAddElim : CommandElab := fun stx => do
+  match stx with
+  | `(norm_cast_add_elim $id:ident) =>
+    Elab.Command.liftCoreM do MetaM.run' do
+     addElim (← resolveGlobalConstNoOverload id)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.NormCast