feat: add command norm_cast_add_elim

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

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