cheapest way to disregard `unsafe`

Stream: lean4

[Scott Morrison]

I have an unsafe function, which I'm only ever going to call from meta code. What is the simplest mechanism to cope with the unsafe keyword? As an example, how do I make this run:

unsafe def foo := 37

syntax "foobar" : tactic

open Elab.Tactic Elab Tactic in
elab_rules : tactic | `(tactic| foobar) => do
  let n := foo
  replaceMainGoal [← getMainGoal]

Am I just meant to use implemented_by with a noop for the complicated reality of foo?

unsafe def foo := 37
@[implemented_by foo] def bar := 0

syntax "foobar" : tactic

open Elab.Tactic Elab Tactic in
elab_rules : tactic | `(tactic| foobar) => do
  let n := bar
  logInfo s!"{n}"
  replaceMainGoal [← getMainGoal]

example : True := by
  foobar -- prints 37 still
  trivial

[Scott Morrison]

If there's some way to just decorate the elab_rules to allow it to make unsafe declarations I'd be happier with that.

[Sebastian Ullrich]

You can use docs4#Std.TermUnsafe.termUnsafe_ as in => unsafe do