Matching on Exprs

Stream: lean4

[Jannis Limperg]

I want to check that a constant has a specific type (in my application, MVarId -> MetaM (List MVarId)). In Lean 3, I would match the constant's type against the pattern `(MVarId -> MetaM (List MVarId)). In Lean 4, afaict these expression quotations are not a thing any more, so what are my options (ideally in MetaM or lower)? I can think of a couple of inelegant solutions, but I'm sure you have something elegant as well.

[Sebastian Ullrich]

In Lean core, we usually put such a type behind an abbreviation and then check for the abbreviation name literally. But for true quotations you should take a look at @Gabriel Ebner's https://github.com/gebner/quote4

[Jannis Limperg]

All right, thanks. I'll use the abbrev hack for now to avoid the dependency, but Gabriel's quotations look very cool.