Zulip Chat Archive

Stream: lean4

Topic: Syntax quotation

Frédéric Dupuis (Dec 27 2022 at 21:49):

I have a quick question: what's right way to do this (in the TacticM monad)?

for decl in ←getLCtx do
  let declIdent := mkIdent decl.userName
  evalTactic (← `(tactic| simp at $declIdent))

Last updated: Dec 20 2023 at 11:08 UTC