[Lean] Name-rendering should strip the prefix of the current file

[clementblaudeau]

Lean name rendering always returns fully qualified names, even in the file that defines them. Instead, we should strip names of the prefix of the current file. For instance (in this snippet on the playground):

structure Playground.S1 where
  f1 : USize
  f2 : USize

structure Playground.S2 where
  f1 : Playground.S1
  f2 : USize

def Playground.normal_structs (_ : Rust_primitives.Hax.Tuple0)
  : Result Rust_primitives.Hax.Tuple0 := do
  let
    (s1 : Playground.S1)
    ← (pure (Playground.S1.mk (f1 := (0 : USize)) (f2 := (1 : USize))));
  let
    (s2 : Playground.S2)
    ← (pure
    (Playground.S2.mk
    (f1 := (Playground.S1.mk (f1 := (2 : USize)) (f2 := (3 : USize))))
    (f2 := (4 : USize))));
  Rust_primitives.Hax.Tuple0.mk

Should become (inside the Playground.lean file)

structure S1 where
  f1 : USize
  f2 : USize

structure S2 where
  f1 : S1
  f2 : USize

def normal_structs (_ : Rust_primitives.Hax.Tuple0)
  : Result Rust_primitives.Hax.Tuple0 := do
  let (s1 : S1) ← (pure (S1.mk (f1 := (0 : USize)) (f2 := (1 : USize))));
  let (s2 : S2) ← (pure
    (S2.mk
      (f1 := (S1.mk (f1 := (2 : USize)) (f2 := (3 : USize))))
      (f2 := (4 : USize))));
  Rust_primitives.Hax.Tuple0.mk