Changelog

Unreleased

Post-0.2 development toward the next experimental API boundary.

Introduced structured Theoria.Equation.Identity identities for ordinary, unfold, matcher, and indexed matcher equations.
Removed generated equation declaration atoms; installed generated equations now use structured Theoria.Equation.Identity values as environment keys.
Added Theoria.Equation.Realized so generated equation checking is an anonymous artifact phase before optional theorem installation.
Added selector-based indexed matcher equation lookup/realization and opt-in Vec indexed equation theorem installation.
Added indexed matcher equation identity metadata recording in opt-in Vec environments.
Carried structured equation identities through rewrite/simp rule metadata and friendly CLI/Lean labels.
Added proof-aware rewrite rule fields for future proof-producing simp traces.
Split indexed matcher packages into explicit statement, lemma, realization, and installation phases.
Added explicit indexed matcher rewrite/simp database constructors behind opt-in policy.
Generated the Lean oracle mirror declaration for the validation Vec matcher from the checked matcher type.

Second experimental release after the initial Hex publication.

Hardened equation/matcher metadata validation and registry checks.
Added in-memory equation registry snapshots and centralized generated-theorem realization.
Derived matcher descriptors from checked recursor metadata for the supported Bool/Nat/List fragment.
Added architecture regression tests for equation/matcher layering.
Added release-boundary documentation and clearer experimental/internal API labels.

Initial experimental release.

Added a small dependent proof/spec kernel with explicit checked environments.
Added core terms, normalization, local definitions, universe parameters, equality, and theorem declarations.
Added theorem modules and Mix tasks for theorem validation and installation workflows.
Added Logic, Equality, Bool, Nat, List, and Vec libraries with theorem corpora.
Added inductive specifications, generated recursors/inductors, checked metadata, and iota reduction.
Added native validation via mix theoria.check and mix theoria.validate.
Added contributor-only Lean oracle validation via generated Lean source.
Added internal equation compiler metadata for supported Bool/Nat/List definitions.
Added checked matcher declarations, generated ordinary equations, matcher equations, unfold equations, and registry validation.
Added experimental rewrite and simp groundwork consuming generated equation metadata.
Added ExDoc guides, CI, Reach architecture checks, Credo, ExDNA, Dialyzer, and docs build validation.