structure Lean.Elab.Frontend.State : Type

• commandState : Lean.Elab.Command.State
• parserState : Lean.Parser.ModuleParserState
• cmdPos : String.Pos
• commands : Array Lean.Syntax

theorem Lean.Elab.Frontend.instNonemptyState : Nonempty Lean.Elab.Frontend.State

structure Lean.Elab.Frontend.Context : Type

• inputCtx : Lean.Parser.InputContext

@[reducible, inline]

abbrev Lean.Elab.Frontend.FrontendM (α : Type) : Type

Equations

• Lean.Elab.Frontend.FrontendM = ReaderT Lean.Elab.Frontend.Context (StateRefT' IO.RealWorld Lean.Elab.Frontend.State IO)

def Lean.Elab.Frontend.setCommandState (commandState : Lean.Elab.Command.State) : Lean.Elab.Frontend.FrontendM Unit

@[inline]

def Lean.Elab.Frontend.runCommandElabM {α : Type} (x : Lean.Elab.Command.CommandElabM α) : Lean.Elab.Frontend.FrontendM α

Equations

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

def Lean.Elab.Frontend.elabCommandAtFrontend (stx : Lean.Syntax) : Lean.Elab.Frontend.FrontendM Unit

def Lean.Elab.Frontend.updateCmdPos : Lean.Elab.Frontend.FrontendM Unit

def Lean.Elab.Frontend.getParserState : Lean.Elab.Frontend.FrontendM Lean.Parser.ModuleParserState

Equations

• Lean.Elab.Frontend.getParserState = do let __do_lift ← get pure __do_lift.parserState

def Lean.Elab.Frontend.getCommandState : Lean.Elab.Frontend.FrontendM Lean.Elab.Command.State

Equations

• Lean.Elab.Frontend.getCommandState = do let __do_lift ← get pure __do_lift.commandState

def Lean.Elab.Frontend.setParserState (ps : Lean.Parser.ModuleParserState) : Lean.Elab.Frontend.FrontendM Unit

def Lean.Elab.Frontend.setMessages (msgs : Lean.MessageLog) : Lean.Elab.Frontend.FrontendM Unit

Equations

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

def Lean.Elab.Frontend.getInputContext : Lean.Elab.Frontend.FrontendM Lean.Parser.InputContext

def Lean.Elab.Frontend.processCommand : Lean.Elab.Frontend.FrontendM Bool

partial def Lean.Elab.Frontend.processCommands : Lean.Elab.Frontend.FrontendM Unit

structure Lean.Elab.IncrementalStateextends Lean.Elab.Frontend.State : Type

• commandState : Lean.Elab.Command.State
• parserState : Lean.Parser.ModuleParserState
• cmdPos : String.Pos
• commands : Array Lean.Syntax
• inputCtx : Lean.Parser.InputContext
• initialSnap : Lean.Language.Lean.CommandParsedSnapshot

theorem Lean.Elab.instNonemptyIncrementalState : Nonempty Lean.Elab.IncrementalState

def Lean.Elab.IO.processCommandsIncrementally (inputCtx : Lean.Parser.InputContext) (parserState : Lean.Parser.ModuleParserState) (commandState : Lean.Elab.Command.State) (old? : Option Lean.Elab.IncrementalState) : BaseIO Lean.Elab.IncrementalState

Variant of IO.processCommands that allows for potential incremental reuse. Pass in the result of a previous invocation done with the same state (but usually different input context) to allow for reuse.

partial def Lean.Elab.IO.processCommandsIncrementally.go (inputCtx : Lean.Parser.InputContext) (initialSnap : Lean.Language.Lean.CommandParsedSnapshot) (t : Task Lean.Language.Lean.CommandParsedSnapshot) (commands : Array Lean.Language.Lean.CommandParsedSnapshot) : BaseIO Lean.Elab.IncrementalState

def Lean.Elab.IO.processCommands (inputCtx : Lean.Parser.InputContext) (parserState : Lean.Parser.ModuleParserState) (commandState : Lean.Elab.Command.State) : IO Lean.Elab.Frontend.State

def Lean.Elab.process (input : String) (env : Lean.Environment) (opts : Lean.Options) (fileName : Option String := none) : IO (Lean.Environment × Lean.MessageLog)

@[export lean_run_frontend]

def Lean.Elab.runFrontend (input : String) (opts : Lean.Options) (fileName : String) (mainModuleName : Lean.Name) (trustLevel : UInt32 := 0) (ileanFileName? : Option String := none) (jsonOutput : Bool := false) : IO (Lean.Environment × Bool)

Equations

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