Documentation

Lean.Compiler.FFI

Return C compiler flags for including Lean's headers. Unlike getCFlags, this does not contain the Lean include directory.

Equations
    Instances For

      Return C compiler flags for including Lean's headers.

      Equations
        Instances For

          Return C compiler flags needed to use the C compiler bundled with the Lean toolchain.

          Equations
            Instances For

              Return linker flags for linking against Lean's libraries. Unlike getLinkerFlags, this does not contain the Lean library directory.

              Equations
                Instances For
                  def Lean.Compiler.FFI.getLinkerFlags (leanSysroot : System.FilePath) (linkStatic : Bool := true) :

                  Return linker flags for linking against Lean's libraries.

                  Equations
                    Instances For

                      Return linker flags needed to use the linker bundled with the Lean toolchain.

                      Equations
                        Instances For