feat: upstreaming the json% term elaborator (#3265)

This is used in the "Try this:" widget machinery powering `simp?`.

There is a test file in Std, which I am not upstreaming at the same
time, as that relies on more code actions / #guard_msgs material. That
test file will still of course test things from Std, and later it can be
reunited with the code it is testing.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>