Zulip Chat Archive

Stream: lean4

Topic: Macro expansion in tactics


Wojciech Nawrocki (Nov 05 2022 at 21:02):

I was surprised to see the macro rule

syntax "repeat " tacticSeq : tactic
macro_rules
  | `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip)

which looks like it would obviously loop! From the fact that it doesn't, do I understand correctly that tactic macros are only expanded during runtime, if needed? I.e. if ($seq); fails, then repeat $seq is never expanded? Or is the rule something different but such that this still makes sense?

Gabriel Ebner (Nov 05 2022 at 22:25):

Macro expansion is like WHNF reduction, it only happens at the top-level. And first|and co. only macro-expand the arguments if necessary.

Gabriel Ebner (Nov 05 2022 at 22:27):

(Try to think of tactic evaluation more like term elaboration and less like writing a program, if that helps.)


Last updated: Dec 20 2023 at 11:08 UTC