Recent work proposed defining type-safe macros via interpretation into a multi-stage language. The utility of this approach wasillustrated with a language called MacroML, in which all type checking is carried out before macro expansion. Building on this work, thegoal of this paper is to develop a macro language that makes it easy forprogrammers to reason about terms locally. We show that defining thesemantics of macros in this manner helps in developing and verifyingnot only type systems for macro languages but also equational reasoning principles. Because the MacroML calculus is sensetive to renamingof (what appear locally to be) bound variables, we present a calculus ofstaged notational definitions (SND) that eliminates the renaming problem but retains MacroML’s phase distinction. Additionally, SND incorporates the generality of Griffin’s account of notational definitions. Weexhibit a formal equational theory for SND and prove its soundness.