Remark: MonadQuotation class is part of the Init package and loaded by default since it is used in the builtin command macro.

structure Lean.Unhygienic.Context : Type

• ref : Lean.Syntax
• scope : Lean.MacroScope

@[reducible, inline]

abbrev Lean.Unhygienic (α : Type) : Type

Simplistic MonadQuotation that does not guarantee globally fresh names, that is, between different runs of this or other MonadQuotation implementations. It is only safe if the syntax quotations do not introduce bindings around antiquotations, and if references to globals are prefixed with _root_. (which is not allowed to refer to a local variable) Unhygienic can also be seen as a model implementation of MonadQuotation (since it is completely hygienic as long as it is "run" only once and can assume that there are no other implementations in use, as is the case for the elaboration monads that carry their macro scope state through the entire processing of a file). It uses the state monad to query and allocate the next macro scope, and uses the reader monad to store the stack of scopes corresponding to withFreshMacroScope calls.

Equations

• Lean.Unhygienic = ReaderT Lean.Unhygienic.Context (StateM Lean.MacroScope)

instance Lean.Unhygienic.instMonadQuotation : Lean.MonadQuotation Lean.Unhygienic

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Unhygienic.run {α : Type} (x : Lean.Unhygienic α) : α

Equations

• x.run = StateT.run' (x { ref := Lean.Syntax.missing, scope := Lean.firstFrontendMacroScope }) (Lean.firstFrontendMacroScope + 1)

opaque Lean.pp.sanitizeNames : Lean.Option Bool

def Lean.getSanitizeNames (o : Lean.Options) : Bool

Equations

• Lean.getSanitizeNames o = Lean.Option.get o Lean.pp.sanitizeNames

structure Lean.NameSanitizerState : Type

• options : Lean.Options
• nameStem2Idx : Lean.NameMap Nat

  x ~> 2 if we're already using x✝, x✝¹

• userName2Sanitized : Lean.NameMap Lean.Name

  x._hyg... ~> x✝

def Lean.sanitizeName (userName : Lean.Name) : StateM Lean.NameSanitizerState Lean.Name

Erase macro scopes from userName and add "tombstone" + superscript (or ._hyg).

Equations

• One or more equations did not get rendered due to their size.

def Lean.sanitizeSyntax (stx : Lean.Syntax) : StateM Lean.NameSanitizerState Lean.Syntax

Equations

• Lean.sanitizeSyntax stx = do let __do_lift ← get if Lean.getSanitizeNames __do_lift.options = true then Lean.sanitizeSyntaxAux✝ stx else pure stx