Theoria.Lean.Mirror.Inductive (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3. Generates small Lean mirror declarations from Theoria inductive specs.

Summary

source(spec)

Renders a Lean inductive declaration for the supported oracle fragment.

source!(spec)

Renders a Lean inductive declaration or raises if unsupported.

supports?(spec)

Returns true when the oracle generator supports this inductive shape.

Returns a short reason when source/1 cannot render a spec.

@spec source(Theoria.Inductive.Spec.t()) :: {:ok, String.t()} | {:error, String.t()}

Renders a Lean inductive declaration for the supported oracle fragment.

@spec source!(Theoria.Inductive.Spec.t()) :: String.t()

Renders a Lean inductive declaration or raises if unsupported.

@spec supports?(Theoria.Inductive.Spec.t()) :: boolean()

Returns true when the oracle generator supports this inductive shape.

@spec unsupported_reason(Theoria.Inductive.Spec.t()) :: String.t() | nil

Returns a short reason when source/1 cannot render a spec.