Pre-expressions

Stream: general

[Dan Velleman]

I don't really understand what I'm allowed to use in a pre-expression. In a tactic I'm writing now, I find that I can write (trans %%H1 %%H2) to define a pre-expression, but if I write (eq.trans %%H1 %%H2) I get the error "unexpected local in quotation expression". Why?

[Dan Velleman]

Oops, it looks like the backquotes didn't come through in my post. I had two backquotes before both open parentheses.

[Yaël Dillies]

You can always use more backticks in Zulip :wink:

[Rob Lewis]

Dan Velleman said:

I don't really understand what I'm allowed to use in a pre-expression. In a tactic I'm writing now, I find that I can write ``(trans %%H1 %%H2) to define a pre-expression, but if I write ``(eq.trans %%H1 %%H2) I get the error "unexpected local in quotation expression". Why?

Hard to say without more context. What are the types of H1 and H2? Can you create a #mwe?

[Dan Velleman]

H1 and H2 have type expr. I'll try to create a mwe.

[Dan Velleman]

Oh, stupid mistake: In my tactic, I had named a local variable eq. I changed it to eqn and that fixed it.