Theoria.Lean.Module (theoria v0.3.0)

Copy Markdown View Source

Experimental/internal API for 0.2; subject to change before 0.3. Builds Lean oracle source files from encoded checks.

Summary

Types

check()
stats()
t()

Functions

add_defeq_check(module, name, left, right)

Adds a definitional-equality check, rendered as example : left = right := rfl.

add_proof_check(module, name, proof, type)

Adds a proof check, rendered as example : type := proof.

add_type_check(module, name, type)

Adds a type check, rendered as #check (type) for shape validation.

from_validation(validation)

Builds a Lean module from Theoria's validation corpus.

new()

Creates an empty Lean oracle module.

render(module)

Renders the complete Lean source file.

stats(module)

Returns proof/defeq check counts.

Types

check()

@type check() ::
  {:proof, String.t(), Theoria.Term.t(), Theoria.Term.t()}
  | {:defeq, String.t(), Theoria.Term.t(), Theoria.Term.t()}
  | {:type, String.t(), Theoria.Term.t()}

stats()

@type stats() :: %{
  proof: non_neg_integer(),
  defeq: non_neg_integer(),
  type: non_neg_integer(),
  total: non_neg_integer()
}

t()

@type t() :: %Theoria.Lean.Module{checks: [check()]}

Functions

add_defeq_check(module, name, left, right)

@spec add_defeq_check(t(), String.t(), Theoria.Term.t(), Theoria.Term.t()) :: t()

Adds a definitional-equality check, rendered as example : left = right := rfl.

add_proof_check(module, name, proof, type)

@spec add_proof_check(t(), String.t(), Theoria.Term.t(), Theoria.Term.t()) :: t()

Adds a proof check, rendered as example : type := proof.

add_type_check(module, name, type)

@spec add_type_check(t(), String.t(), Theoria.Term.t()) :: t()

Adds a type check, rendered as #check (type) for shape validation.

from_validation(validation)

@spec from_validation(Theoria.Validation.Corpus.t()) :: {:ok, t()} | {:error, term()}

Builds a Lean module from Theoria's validation corpus.

new()

@spec new() :: t()

Creates an empty Lean oracle module.

render(module)

@spec render(t()) :: String.t()

Renders the complete Lean source file.

stats(module)

@spec stats(t()) :: stats()

Returns proof/defeq check counts.