Syntactic sugar for .deep_view()

[dschoepe]

During the last two Verus retreats, we discussed that a shorthand for .deep_view() similar to @ for .view() would be useful. Let's use this discussion to get feedback on whether that would be helpful and, if so, what syntax we'd like to use for this.

[parno]

Previously nominated symbols have included: ~, #, .@, @, *@, (@), \@, ~@. We'd like to find something that's easy to parse (and that doesn't create parsing ambiguities).