Feature suggestion: {leanWithScope}

[nomeata]

As a short-hand to quickly get some variables into scope locally for proper highlighting, it would be nice to do that within {lean} or a variant thereof. Syntax ideas:

Lorem ipsum `{leanWithScope}`fun (x : Nat) (xs : List Nat) => x ∈ xs` -- explicit lambdaTelescope
Lorem ipsum `{lean}`(x : Nat) (xs : List Nat) : x ∈ xs`               -- if this isn’t too ambiguous
Lorem ipsum `{lean}`(x : Nat) (xs : List Nat) |- x ∈ xs             ` -- hoping this doesn’t conflict