Documentation

Lean.Elab.Frontend

source
structure Lean.Elab.Frontend.State :
Type
Instances For
source
instance Lean.Elab.Frontend.instNonemptyState :
Nonempty Lean.Elab.Frontend.State
Equations
source
structure Lean.Elab.Frontend.Context :
Type
source
@[reducible, inline]
abbrev Lean.Elab.Frontend.FrontendM (α : Type) :
Type
Equations
source
def Lean.Elab.Frontend.setCommandState (commandState : Lean.Elab.Command.State) :
Lean.Elab.Frontend.FrontendM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
@[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.
source
def Lean.Elab.Frontend.elabCommandAtFrontend (stx : Lean.Syntax) :
Lean.Elab.Frontend.FrontendM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Frontend.updateCmdPos :
Lean.Elab.Frontend.FrontendM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Frontend.getParserState :
Lean.Elab.Frontend.FrontendM Lean.Parser.ModuleParserState
Equations
source
def Lean.Elab.Frontend.getCommandState :
Lean.Elab.Frontend.FrontendM Lean.Elab.Command.State
Equations
source
def Lean.Elab.Frontend.setParserState (ps : Lean.Parser.ModuleParserState) :
Lean.Elab.Frontend.FrontendM Unit
Equations
source
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.
source
def Lean.Elab.Frontend.getInputContext :
Lean.Elab.Frontend.FrontendM Lean.Parser.InputContext
Equations
source
def Lean.Elab.Frontend.processCommand :
Lean.Elab.Frontend.FrontendM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Frontend.processCommands :
Lean.Elab.Frontend.FrontendM Unit
source
def Lean.Elab.IO.processCommands (inputCtx : Lean.Parser.InputContext) (parserState : Lean.Parser.ModuleParserState) (commandState : Lean.Elab.Command.State) :
IO Lean.Elab.Frontend.State
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Elab.IncrementalStateextends Lean.Elab.Frontend.State :
Type
Instances For
source
instance Lean.Elab.instNonemptyIncrementalState :
Nonempty Lean.Elab.IncrementalState
Equations
source
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 uses the new Lean language processor implementation for potential incremental reuse. Pass in result of a previous invocation done with the same state (but usually different input context) to allow for reuse.

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.IO.processCommandsIncrementally.go (inputCtx : Lean.Parser.InputContext) (initialSnap : Lean.Language.Lean.CommandParsedSnapshot) (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) (commands : Array Lean.Syntax) :
BaseIO Lean.Elab.IncrementalState
source
def Lean.Elab.process (input : String) (env : Lean.Environment) (opts : Lean.Options) (fileName : optParam (Option String) none) :
IO (Lean.Environment × Lean.MessageLog)
Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_run_frontend]
def Lean.Elab.runFrontend (input : String) (opts : Lean.Options) (fileName : String) (mainModuleName : Lake.Name) (trustLevel : optParam UInt32 0) (ileanFileName? : optParam (Option String) none) (jsonOutput : optParam Bool false) :
IO (Lean.Environment × Bool)
Equations
  • One or more equations did not get rendered due to their size.