Documentation

Lean.Elab.Frontend

Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

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.

Equations
  • One or more equations did not get rendered due to their size.
Equations
def Lean.Elab.process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) :
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_run_frontend]
def Lean.Elab.runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 0) (ileanFileName? : Option String := none) (jsonOutput : Bool := false) (errorOnKinds : Array Name := #[]) :
Equations
  • One or more equations did not get rendered due to their size.