source
def Lean.Syntax.prettyPrint (stx : Syntax) :
Format
Equations

- stx.prettyPrint = match stx.unsetTrailing.reprint with | some str => Std.format str.toFormat | none => Std.format stx

Instances For

source
def Lean.MacroScopesView.format (view : MacroScopesView) (mainModule : Name) :
Format
Equations

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

Instances For

source
def Lean.MacroScopesView.equalScope (a b : MacroScopesView) :
Bool

Two names are from the same lexical scope if their scoping information modulo `MacroScopesView.name` is equal.

Equations

- a.equalScope b = (a.scopes == b.scopes && a.ctx == b.ctx && a.imported == b.imported)

Instances For

source
def Lean.Elab.expandOptNamedPrio (stx : Syntax) :
MacroM Nat
Equations

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

Instances For

source
structure Lean.Elab.MacroStackElem :
Type

- before : Syntax
- after : Syntax

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.MacroStack :
Type
Equations

- Lean.Elab.MacroStack = List Lean.Elab.MacroStackElem

Instances For

source
def Lean.Elab.getBetterRef (ref : Syntax) (macroStack : MacroStack) :
Syntax

If `ref` does not have position information, then try to use macroStack

Equations

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

Instances For

source
opaque Lean.Elab.pp.macroStack :
Lean.Option Bool
source
def Lean.Elab.addMacroStack {m : Type → Type} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) :
m MessageData
Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.addMacroStack msgData [] = do let __do_lift ← Lean.getOptions if (!Lean.Option.get __do_lift Lean.Elab.pp.macroStack) = true then pure msgData else pure msgData

Instances For

source
def Lean.Elab.checkSyntaxNodeKind {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (k : Name) :
m Name
Equations

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

Instances For

source
def Lean.Elab.checkSyntaxNodeKindAtNamespaces {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (k : Name) :
Name → m Name
Equations

- Lean.Elab.checkSyntaxNodeKindAtNamespaces k (p.str str) = (Lean.Elab.checkSyntaxNodeKind (p.str str ++ k) <|> Lean.Elab.checkSyntaxNodeKindAtNamespaces k p)
- Lean.Elab.checkSyntaxNodeKindAtNamespaces k Lean.Name.anonymous = Lean.Elab.checkSyntaxNodeKind k
- Lean.Elab.checkSyntaxNodeKindAtNamespaces k x✝ = Lean.throwError (Lean.toMessageData "failed")

Instances For

source
def Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces (k : Name) :
AttrM Name
Equations

- Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces k = do let ctx ← read Lean.Elab.checkSyntaxNodeKindAtNamespaces k ctx.currNamespace

Instances For

source
def Lean.Elab.syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (stx : Syntax) :
AttrM SyntaxNodeKind
Equations

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

Instances For

source
@[implemented_by _private.Lean.Elab.Util.0.Lean.Elab.evalSyntaxConstantUnsafe]
opaque Lean.Elab.evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) :
ExceptT String Id Syntax
source
unsafe def Lean.Elab.mkElabAttribute (γ : Type) (attrBuiltinName attrName parserNamespace typeName : Name) (kind : String) (attrDeclName : Name := by exact decl_name%) :
IO (KeyedDeclsAttribute γ)
Equations

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

Instances For

source
unsafe def Lean.Elab.mkMacroAttributeUnsafe (ref : Name) :
IO (KeyedDeclsAttribute Macro)
Equations

- Lean.Elab.mkMacroAttributeUnsafe ref = Lean.Elab.mkElabAttribute Lean.Macro `builtin_macro `macro Lean.Name.anonymous `Lean.Macro "macro" ref

Instances For

source
@[implemented_by Lean.Elab.mkMacroAttributeUnsafe]
opaque Lean.Elab.mkMacroAttribute (ref : Name) :
IO (KeyedDeclsAttribute Macro)
source
opaque Lean.Elab.macroAttribute :
KeyedDeclsAttribute Macro

Registers a macro expander for a given syntax node kind.

A macro expander should have type `Lean.Macro` (which is `Lean.Syntax → Lean.MacroM Lean.Syntax`), i.e. should take syntax of the given syntax node kind as a parameter and produce different syntax in the same syntax category.

The `macro_rules` and `macro` commands should usually be preferred over using this attribute directly.

source
def Lean.Elab.expandMacroImpl? (env : Environment) :
Syntax → MacroM (Option (Name × Except Macro.Exception Syntax))

Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful. Return none if all macros threw `Macro.Exception.unsupportedSyntax`.

Equations

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

Instances For

source
class Lean.Elab.MonadMacroAdapter (m : Type → Type) extends Lean.MonadQuotation m :
Type 1

- getRef : m Syntax
- withRef {α : Type} : Syntax → m α → m α
- getCurrMacroScope : m MacroScope
- getContext : m Name
- withFreshMacroScope {α : Type} : m α → m α
- getNextMacroScope : m MacroScope
- setNextMacroScope : MacroScope → m Unit

Instances

source
@[always_inline]
instance Lean.Elab.instMonadMacroAdapterOfMonadLiftOfMonadQuotation (m n : Type → Type) [MonadLift m n] [MonadQuotation n] [MonadMacroAdapter m] :
MonadMacroAdapter n
Equations

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

source
def Lean.Elab.liftMacroM {m : Type → Type} {α : Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) :
m α
Equations

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

Instances For

source
@[inline]
def Lean.Elab.adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : Macro) (stx : Syntax) :
m Syntax
Equations

- Lean.Elab.adaptMacro x stx = Lean.Elab.liftMacroM (x stx)

Instances For

source
def Lean.Elab.mkUnusedBaseName (baseName : Name) :
MacroM Name
Equations

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

Instances For

source
def Lean.Elab.logException {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m] (ex : Exception) :
m Unit
Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.logException (Lean.Exception.error ref msg) = Lean.logErrorAt ref msg

Instances For

source
def Lean.Elab.withLogging {m : Type → Type} [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m] (x : m Unit) :
m Unit

If `x` throws an exception, catch it and turn it into a log message (using `logException`).

Equations

- Lean.Elab.withLogging x = tryCatch x fun (ex : Lean.Exception) => Lean.Elab.logException ex

Instances For

source
def Lean.Elab.nestedExceptionToMessageData {m : Type → Type} [Monad m] [MonadLog m] (ex : Exception) :
m MessageData
Equations

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

Instances For

source
def Lean.Elab.throwErrorWithNestedErrors {m : Type → Type} {α : Type} [MonadError m] [Monad m] [MonadLog m] (msg : MessageData) (exs : Array Exception) :
m α
Equations

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

Instances For