unknown identifier '__stx_lift✝'

Stream: lean4

[James Gallicchio]

I'm writing some pretty normal-looking (but wrong) quotations and getting a deeply unhelpful unknown identifier '__stx_lift✝' error.

Before I try MWE'ing, has anyone else hit that? I suspect Zulip-search could be missing some results :(

[Alex Keizer]

I think I've seen this sort of error before when using inline monadic binds, like in

let foo <- bar (<- a)

[James Gallicchio]

I worked around it by manually lifting enough inline syntax to let binds, but I'm assuming it's a bug? I'll try to minimize.