The 0.3 development line makes generated equation artifacts explicit domain data instead of public generated atoms.
Equation identities
Theoria.Equation.Identity is the canonical identity for generated equation artifacts:
alias Theoria.Equation.Identity
Identity.equation(:nat_add, :succ)
Identity.unfold(:nat_add)
Identity.matcher_equation(:nat_add_match_1, :succ)
Identity.indexed_matcher_equation(:vec_match, :vec_cons)Friendly output still renders familiar labels such as nat_add.eq_succ, but those labels are display strings. When generated equation theorems are installed, the structured Identity value itself is used as the environment key; generated atom encodings are not part of the model.
Matcher names
Generated matcher declarations currently remain atoms such as :nat_add_match_1. Use Theoria.Equation.Matcher.Info.default_name/2 and source_name/1 instead of hand-building or parsing those names.
Indexed Vec matcher opt-in
Prelude.env/0 does not install indexed matchers or indexed matcher equations.
For validation and experiments, Vec exposes an explicit opt-in path:
Theoria.Library.Vec.env_with_indexed_matcher()
Theoria.Library.Vec.env_with_indexed_matcher(install_equations: true)The second form also installs realized indexed equation theorem declarations and records them in the matcher metadata. Rewrite and simp still exclude indexed matcher equations by default; pass include_indexed_matchers: true or use the indexed-specific database constructors when experimenting.
Stability
This line is still experimental. The trusted kernel boundary is unchanged; equation generation, matcher planning, rewrite/simp, and Lean oracle output remain untrusted helpers whose products matter only after native kernel checking.