Theoria.Lean.Oracle (theoria v0.4.0)

Copy Markdown View Source

Experimental/internal API for 0.2; subject to change before 0.3. Runs generated Lean oracle files for contributor validation.

Summary

Functions

lean_executable(opts \\ [])

Returns the Lean executable path, if available.

run(source, opts \\ [])

Writes source and checks it with Lean.

Functions

lean_executable(opts \\ [])

@spec lean_executable(keyword()) :: {:ok, String.t()} | {:error, :lean_not_found}

Returns the Lean executable path, if available.

run(source, opts \\ [])

@spec run(
  String.t(),
  keyword()
) :: {:ok, map()} | {:error, term()}

Writes source and checks it with Lean.