Documentation

Lean.Elab.Frontend

structure Lean.Elab.Frontend.State :
Type
Equations
@[inline]
Equations
Equations
Equations
Equations
Equations
  • Lean.Elab.Frontend.setMessages msgs = modify fun s => { commandState := let src := s.commandState; { env := src.env, messages := msgs, scopes := src.scopes, nextMacroScope := src.nextMacroScope, maxRecDepth := src.maxRecDepth, nextInstIdx := src.nextInstIdx, ngen := src.ngen, infoState := src.infoState, traceState := src.traceState }, parserState := s.parserState, cmdPos := s.cmdPos, commands := s.commands }
Equations
Equations
Equations
def Lean.Elab.runFrontend (input : String) (opts : Lean.Options) (fileName : String) (mainModuleName : Lean.Name) (trustLevel : optParam UInt32 0) (ileanFileName? : optParam (Option String) none) :
Equations