TermElabM expected type

Stream: lean4

[Thomas Vigouroux]

Hi,

In a TermElabM monad, is there a way to check is the expected term's type is of a certain form, i.e MyType a b while capturing a and b ?

[Henrik Böving]

If you have the expected type available you can pattern match on it with match_expr

[Thomas Vigouroux]

Not sure if I have it or not.

Basically I have written a parser Parsec ... and I'd like to embed it in an elaborator so that I can parse things into expressions

[Thomas Vigouroux]

Not sure I am clear

[Thomas Vigouroux]

I have been writting a bunch of ToExpr instances to convert my actual value to an Expr already