converting between `[foo] and "foo"

Stream: general

[Scott Morrison]

I'm finding myself needing both the pexprs: `[foo] and "foo". Does anyone know how to convert in either direction?

[Rob Lewis]

I don't think this is really doable. Check the output of run_cmd trace $ ``(`[simp])

[Floris van Doorn]

I think this converts "foo" to `[foo]:

open tactic lean lean.parser interactive

@[user_command] meta def add_hint (_ : parse (tk "add_hint")) : parser unit :=
do n ← parser.pexpr,
   n ← to_expr n,
   s ← eval_expr string n,
   let t := "`[" ++ s ++ "]",
   t ← with_input parser.pexpr t,
   trace s,
   trace t,
   skip

open tactic

add_hint "simp"

[Scott Morrison]

Thanks.