Documentation

Lean.Hygiene

source
structure Lean.Unhygienic.Context:
Type
source
@[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 implentations 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
source
instance Lean.Unhygienic.instMonadQuotationUnhygienic:
Lean.MonadQuotation Lean.Unhygienic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Unhygienic.run {α : Type} (x : Lean.Unhygienic α) :
α
Equations
source
opaque Lean.pp.sanitizeNames:
Lean.Option Bool
source
def Lean.getSanitizeNames (o : Lean.Options) :
Bool
Equations
source
structure Lean.NameSanitizerState:
Type
source
def Lean.sanitizeName (userName : Lean.Name) :
StateM Lean.NameSanitizerState Lean.Name
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.sanitizeSyntax (stx : Lean.Syntax) :
StateM Lean.NameSanitizerState Lean.Syntax
Equations