Documentation

Lean.Elab.Frontend

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

                    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.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Parses values of options registered during import and left by the C++ frontend as strings, fails if any option names remain unknown.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[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) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For