[Lean] Lean backend renders functions with `hax_lib::opaque` as `Rust_primitives.Hax.dropped_body`

[abentkamp]

#[hax_lib::opaque]
pub fn hello() {}

Open this code snippet in the playground

Actual Lean output:

def Playground.hello
  (_ : Rust_primitives.Hax.Tuple0)
  : RustM Rust_primitives.Hax.Tuple0
  := do
  (pure Rust_primitives.Hax.dropped_body)

Expected Lean output:

opaque Playground.hello
  (_ : Rust_primitives.Hax.Tuple0)
  : RustM Rust_primitives.Hax.Tuple0