# theoria v0.3.0 - Table of Contents

> An Elixir-native proof/spec kernel inspired by trusted theorem prover kernels.

## Pages

- [Theoria](readme.md)
- [Changelog](changelog.md)
- [LICENSE](license.md)

- Guides
  - [0.3 development boundary](release_0_3.md)
  - [Theoria 0.2 release boundary](release_0_2.md)
  - [Theoria Design](design.md)
  - [Inductive specifications](inductives.md)
  - [Theoria validation](validation.md)
  - [Equation metadata and generated lemmas](equations.md)
  - [Lean oracle validation](lean_validation.md)
  - [Lean alignment notes](lean_alignment.md)
  - [Lean-inspired roadmap](lean_roadmap.md)
  - [Theorem Modules](theorem_modules.md)

## Modules

- [Theoria](Theoria.md): An Elixir-native proof/spec kernel inspired by Lean's trusted-kernel design.
- [Theoria.Env.Constant](Theoria.Env.Constant.md): A checked constant or definition in a kernel environment.
- [Theoria.Env.Constructor](Theoria.Env.Constructor.md): Lean-style metadata for an admitted inductive constructor.
- [Theoria.Env.Inductive](Theoria.Env.Inductive.md): Lean-style metadata for an admitted inductive type former.
- [Theoria.Env.Matcher](Theoria.Env.Matcher.md): Environment metadata for a generated matcher declaration.
- [Theoria.Env.Recursor](Theoria.Env.Recursor.md): Lean-style metadata for an admitted inductive recursor.
- [Theoria.Env.RecursorRule](Theoria.Env.RecursorRule.md): Lean-style iota-reduction rule metadata for a recursor constructor case.
- [Theoria.Env.Reduction](Theoria.Env.Reduction.md): Primitive reduction metadata attached to environment declarations.
- [Theoria.Env.Reduction.Iota](Theoria.Env.Reduction.Iota.md): Marks a recursor declaration as using constructor iota-reduction rules.
- [Theoria.Equality](Theoria.Equality.md): Untrusted helpers for building equality transport terms.
- [Theoria.Kernel.RecursorRules](Theoria.Kernel.RecursorRules.md): Validation for trusted recursor iota rules.
- [Theoria.Kernel.TrustReport](Theoria.Kernel.TrustReport.md): Dependency and trust summary for an environment declaration.
- [Theoria.Level](Theoria.Level.md): Universe levels.
- [Theoria.Level.Constraint](Theoria.Level.Constraint.md): Universe-level ordering constraint.
- [Theoria.Level.Max](Theoria.Level.Max.md): Maximum of two universe levels.
- [Theoria.Level.Param](Theoria.Level.Param.md): A universe level parameter.
- [Theoria.Level.Solver](Theoria.Level.Solver.md): Small solver for universe-level ordering constraints.
- [Theoria.Level.Succ](Theoria.Level.Succ.md): Successor universe level.
- [Theoria.Level.Zero](Theoria.Level.Zero.md): The zero universe level.
- [Theoria.Normalize](Theoria.Normalize.md): Normalization and definitional equality for core terms.
- [Theoria.Normalize.Fuel](Theoria.Normalize.Fuel.md): Shared fuel budget for normalization.
- [Theoria.Normalize.Primitive](Theoria.Normalize.Primitive.md): Primitive weak-head reductions for declarations with iota metadata.
- [Theoria.Syntax.App](Theoria.Syntax.App.md): Function application.
- [Theoria.Syntax.Const](Theoria.Syntax.Const.md): A named environment constant.
- [Theoria.Syntax.Eq](Theoria.Syntax.Eq.md): Named-syntax propositional equality.
- [Theoria.Syntax.EqRec](Theoria.Syntax.EqRec.md): Named-syntax equality recursor.
- [Theoria.Syntax.Forall](Theoria.Syntax.Forall.md): Dependent function type with a named binder.
- [Theoria.Syntax.Lam](Theoria.Syntax.Lam.md): Lambda abstraction with a named binder.
- [Theoria.Syntax.Let](Theoria.Syntax.Let.md): Local definition with a named binder.
- [Theoria.Syntax.Refl](Theoria.Syntax.Refl.md): Named-syntax reflexivity proof.
- [Theoria.Syntax.Sort](Theoria.Syntax.Sort.md): A named-syntax universe level.
- [Theoria.Syntax.Var](Theoria.Syntax.Var.md): A named bound variable.
- [Theoria.Term](Theoria.Term.md): Core terms for Theoria's trusted kernel.
- [Theoria.Term.App](Theoria.Term.App.md): Function application.
- [Theoria.Term.Application](Theoria.Term.Application.md): Helpers for application terms.
- [Theoria.Term.BVar](Theoria.Term.BVar.md): A bound variable represented by a de Bruijn index.
- [Theoria.Term.Const](Theoria.Term.Const.md): A named environment constant.
- [Theoria.Term.Eq](Theoria.Term.Eq.md): Propositional equality over a type.
- [Theoria.Term.EqRec](Theoria.Term.EqRec.md): Primitive equality recursor.
- [Theoria.Term.Forall](Theoria.Term.Forall.md): Dependent function type. Non-dependent functions are encoded as forall types.
- [Theoria.Term.Lam](Theoria.Term.Lam.md): Lambda abstraction.
- [Theoria.Term.Let](Theoria.Term.Let.md): Local definition.
- [Theoria.Term.Refl](Theoria.Term.Refl.md): Reflexivity proof for propositional equality.
- [Theoria.Term.Sort](Theoria.Term.Sort.md): A universe level, written `Type n` in the surface language.

- Kernel
  - [Theoria.Context](Theoria.Context.md): Typing context for bound variables.
  - [Theoria.Env](Theoria.Env.md): Kernel environment containing checked constants and definitions.

  - [Theoria.Error](Theoria.Error.md): Kernel error returned when a term cannot be checked.
  - [Theoria.Kernel](Theoria.Kernel.md): The trusted type-checking kernel.

- Syntax
  - [Theoria.DSL](Theoria.DSL.md): Small Elixir DSL for constructing named Theoria syntax terms.
  - [Theoria.Elaborator](Theoria.Elaborator.md): Converts named `Theoria.Syntax` terms to de Bruijn-indexed `Theoria.Term` terms.
  - [Theoria.Pretty](Theoria.Pretty.md): Human-readable rendering for Theoria values.
  - [Theoria.Syntax](Theoria.Syntax.md): Named surface terms for building Theoria core terms.

- Inductives
  - [Theoria.Inductive](Theoria.Inductive.md): Validation helpers for inductive specifications.
  - [Theoria.Inductive.Admission](Theoria.Inductive.Admission.md): Staged admission pipeline for inductive specifications.
  - [Theoria.Inductive.Constructor](Theoria.Inductive.Constructor.md): Constructor declaration in an inductive specification.
  - [Theoria.Inductive.Constructor.Result](Theoria.Inductive.Constructor.Result.md): Decomposed constructor target and binders.
  - [Theoria.Inductive.Declaration](Theoria.Inductive.Declaration.md): Generated declaration plan for an inductive specification.
  - [Theoria.Inductive.Generate](Theoria.Inductive.Generate.md): Generators for declarations derived from inductive specs.
  - [Theoria.Inductive.Index](Theoria.Inductive.Index.md): Named index of an inductive family.
  - [Theoria.Inductive.Parameter](Theoria.Inductive.Parameter.md): Named parameter of an inductive family.
  - [Theoria.Inductive.Recursor](Theoria.Inductive.Recursor.md): Recursor or induction principle declaration in an inductive specification.
  - [Theoria.Inductive.Report](Theoria.Inductive.Report.md): Summary of an inductive declaration plan.
  - [Theoria.Inductive.Shape](Theoria.Inductive.Shape.md): Structured classification of supported inductive shapes.
  - [Theoria.Inductive.Spec](Theoria.Inductive.Spec.md): Structured description of an inductive family.

- Equations
  - [Theoria.Equation](Theoria.Equation.md): Experimental/internal API for 0.2; subject to change before 0.3.
  - [Theoria.Equation.Branch](Theoria.Equation.Branch.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal constructor-specific branch descriptors for equation compilation.
  - [Theoria.Equation.Case.Template](Theoria.Equation.Case.Template.md): Experimental/internal API for 0.2; subject to change before 0.3. Schematic equation case template used by schema generation.
  - [Theoria.Equation.Clause](Theoria.Equation.Clause.md): Experimental/internal API for 0.2; subject to change before 0.3. A constructor equation clause.
  - [Theoria.Equation.Compiled](Theoria.Equation.Compiled.md): Experimental/internal API for 0.2; subject to change before 0.3. Result of compiling constructor equations, including generated metadata.
  - [Theoria.Equation.Compiler](Theoria.Equation.Compiler.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal constructor-equation compiler for the initial Bool/Nat/List fragment.
  - [Theoria.Equation.Context](Theoria.Equation.Context.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal named values available while materializing an equation branch body.
  - [Theoria.Equation.Definition](Theoria.Equation.Definition.md): Experimental/internal API for 0.2; subject to change before 0.3. Small internal helpers for building core lambda definitions.
  - [Theoria.Equation.Definition.Spec](Theoria.Equation.Definition.Spec.md): Experimental/internal API for 0.2; subject to change before 0.3. Complete metadata package for a compiled equation definition.
  - [Theoria.Equation.Eqns](Theoria.Equation.Eqns.md): Experimental/internal API for 0.2; subject to change before 0.3. Lookup helpers for generated equation theorem metadata.
  - [Theoria.Equation.Extension](Theoria.Equation.Extension.md): Experimental/internal API for 0.2; subject to change before 0.3. Typed registry helpers for generated equation and matcher metadata.
  - [Theoria.Equation.Extension.Registry](Theoria.Equation.Extension.Registry.md): In-memory registry snapshot for generated equation metadata.
  - [Theoria.Equation.FixedParams](Theoria.Equation.FixedParams.md): Experimental/internal API for 0.2; subject to change before 0.3. Minimal descriptor for fixed parameters of compiled equation definitions.
  - [Theoria.Equation.Identity](Theoria.Equation.Identity.md): Structured identity for generated equation artifacts.
  - [Theoria.Equation.Info](Theoria.Equation.Info.md): Experimental/internal API for 0.2; subject to change before 0.3. Lean-inspired metadata for a compiled equation definition.
  - [Theoria.Equation.Lemma](Theoria.Equation.Lemma.md): Experimental/internal API for 0.2; subject to change before 0.3. Metadata for an equation lemma generated from compiled equations.
  - [Theoria.Equation.Matcher.Descriptor](Theoria.Equation.Matcher.Descriptor.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal descriptor-driven matcher generation metadata.
  - [Theoria.Equation.Matcher.Descriptor.Alternative](Theoria.Equation.Matcher.Descriptor.Alternative.md): Descriptor for one matcher alternative.
  - [Theoria.Equation.Matcher.Descriptor.Field](Theoria.Equation.Matcher.Descriptor.Field.md): Normalized constructor field shape for matcher descriptors.
  - [Theoria.Equation.Matcher.Eqns](Theoria.Equation.Matcher.Eqns.md): Experimental/internal API for 0.2; subject to change before 0.3. Lookup helpers for generated matcher equation metadata.
  - [Theoria.Equation.Matcher.Equation](Theoria.Equation.Matcher.Equation.md): Experimental/internal API for 0.2; subject to change before 0.3. Metadata for an equation generated for a matcher alternative.
  - [Theoria.Equation.Matcher.Indexed.Package](Theoria.Equation.Matcher.Indexed.Package.md): Experimental/internal API for 0.2; subject to change before 0.3. Coherent package for indexed matcher equation metadata.
  - [Theoria.Equation.Matcher.Indexed.Realization](Theoria.Equation.Matcher.Indexed.Realization.md): Experimental/internal API for 0.2; subject to change before 0.3. Realization planning for indexed matcher equations.
  - [Theoria.Equation.Matcher.Indexed.Realization.EquationPlan](Theoria.Equation.Matcher.Indexed.Realization.EquationPlan.md): Realization plan for one indexed matcher equation.
  - [Theoria.Equation.Matcher.Indexed.Realization.Plan](Theoria.Equation.Matcher.Indexed.Realization.Plan.md): Realization plan for an indexed matcher equation package.
  - [Theoria.Equation.Matcher.Indexed.Vec](Theoria.Equation.Matcher.Indexed.Vec.md): Experimental/internal API for indexed Vec matcher metadata packages.
  - [Theoria.Equation.Matcher.Info](Theoria.Equation.Matcher.Info.md): Experimental/internal API for 0.2; subject to change before 0.3. Small Theoria-side mirror of Lean matcher metadata.
  - [Theoria.Equation.Matcher.Info.Alternative](Theoria.Equation.Matcher.Info.Alternative.md): Metadata for one matcher alternative.
  - [Theoria.Equation.Matcher.Info.Discriminant](Theoria.Equation.Matcher.Info.Discriminant.md): Metadata for one matcher discriminant.
  - [Theoria.Equation.Matcher.Spec](Theoria.Equation.Matcher.Spec.md): Experimental/internal API for 0.2; subject to change before 0.3. Checked declaration package for a generated matcher.
  - [Theoria.Equation.Matcher.Statement](Theoria.Equation.Matcher.Statement.md): Experimental/internal API for 0.2; subject to change before 0.3. Statement planning for matcher equations.
  - [Theoria.Equation.Matcher.Statement.Dispatch](Theoria.Equation.Matcher.Statement.Dispatch.md): Dispatches indexed matcher equation statement planning to family-specific planners.
  - [Theoria.Equation.Matcher.Statement.Frame](Theoria.Equation.Matcher.Statement.Frame.md): Internal binder frame for matcher equation statement planning.
  - [Theoria.Equation.Matcher.Statement.Indexed](Theoria.Equation.Matcher.Statement.Indexed.md): Shared helpers for indexed matcher statement planning.
  - [Theoria.Equation.Matcher.Statement.Vec](Theoria.Equation.Matcher.Statement.Vec.md): Internal indexed Vec statement planner for matcher equations.
  - [Theoria.Equation.Matcher.Type](Theoria.Equation.Matcher.Type.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal builder for checked matcher declaration types and bodies for supported fragments.
  - [Theoria.Equation.Matcher.Type.Alternative](Theoria.Equation.Matcher.Type.Alternative.md): Matcher branch type descriptor.
  - [Theoria.Equation.Matcher.Type.Shape](Theoria.Equation.Matcher.Type.Shape.md): Planned matcher declaration shape derived from a matcher descriptor.
  - [Theoria.Equation.Pattern](Theoria.Equation.Pattern.md): Experimental/internal API for 0.2; subject to change before 0.3. Equation compiler patterns.
  - [Theoria.Equation.Pattern.Constructor](Theoria.Equation.Pattern.Constructor.md): A constructor pattern with subpatterns.
  - [Theoria.Equation.Pattern.Var](Theoria.Equation.Pattern.Var.md): A variable pattern.
  - [Theoria.Equation.Pattern.Wildcard](Theoria.Equation.Pattern.Wildcard.md): A wildcard pattern.
  - [Theoria.Equation.Realized](Theoria.Equation.Realized.md): A kernel-checked generated equation artifact that is not necessarily installed as a theorem.
  - [Theoria.Equation.Recursor.Application](Theoria.Equation.Recursor.Application.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal raw recursor application builders used by the equation compiler.
  - [Theoria.Equation.Recursor.Descriptor](Theoria.Equation.Recursor.Descriptor.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal recursor-derived shape metadata for matcher descriptors.
  - [Theoria.Equation.Recursor.Descriptor.Rule](Theoria.Equation.Recursor.Descriptor.Rule.md): Recursor rule shape used by matcher descriptor generation.
  - [Theoria.Equation.Recursor.Descriptor.Rule.Field](Theoria.Equation.Recursor.Descriptor.Rule.Field.md): Constructor field shape in a recursor rule.
  - [Theoria.Equation.Schema](Theoria.Equation.Schema.md): Experimental/internal API for 0.2; subject to change before 0.3. Schema metadata for generating equation lemmas from compiled definitions.
  - [Theoria.Equation.Schema.Builder](Theoria.Equation.Schema.Builder.md): Experimental/internal API for 0.2; subject to change before 0.3. Internal builder for equation schemas and matcher metadata from signatures and case templates.
  - [Theoria.Equation.Schema.Equation](Theoria.Equation.Schema.Equation.md): One schematic equation theorem generated for a compiled definition.
  - [Theoria.Equation.Signature](Theoria.Equation.Signature.md): Experimental/internal API for 0.2; subject to change before 0.3. Telescope summary for compiler-owned equation metadata generation.
  - [Theoria.Equation.Validator](Theoria.Equation.Validator.md): Experimental/internal API for 0.2; subject to change before 0.3. Validation for constructor-equation clauses.

- Rewrite
  - [Theoria.Rewrite](Theoria.Rewrite.md): Experimental/internal API for 0.2; subject to change before 0.3. Untrusted structural rewrite helpers over core terms.
  - [Theoria.Rewrite.Database](Theoria.Rewrite.Database.md): Experimental/internal API for 0.2; subject to change before 0.3. A tiny untrusted rewrite-rule database.
  - [Theoria.Rewrite.Match](Theoria.Rewrite.Match.md): Experimental/internal API for 0.2; subject to change before 0.3. Untrusted first-order matching for schematic rewrite rules.
  - [Theoria.Rewrite.Rule](Theoria.Rewrite.Rule.md): Experimental/internal API for 0.2; subject to change before 0.3. A theorem-like rewrite rule over a core equality term.
  - [Theoria.Simp](Theoria.Simp.md): Experimental/internal API for 0.2; subject to change before 0.3. Tiny untrusted simplification groundwork backed by generated equation rules.
  - [Theoria.Simp.Database](Theoria.Simp.Database.md): Experimental/internal API for 0.2; subject to change before 0.3. Untrusted simplifier database with rule priorities.
  - [Theoria.Simp.Rule](Theoria.Simp.Rule.md): Experimental/internal API for 0.2; subject to change before 0.3. Simplifier rule metadata layered over untrusted rewrite rules.
  - [Theoria.Simp.Step](Theoria.Simp.Step.md): Experimental/internal API for 0.2; subject to change before 0.3. One simplifier rewrite step for tracing and debugging.

- Validation
  - [Theoria.Validation](Theoria.Validation.md): Runs Theoria-owned validation corpora.
  - [Theoria.Validation.Checkable](Theoria.Validation.Checkable.md): Protocol for running Theoria validation checks.
  - [Theoria.Validation.Core](Theoria.Validation.Core.md): Core calculus validation checks.
  - [Theoria.Validation.Corpus](Theoria.Validation.Corpus.md): Theoria-owned validation corpus consumed by local checks and external oracles.
  - [Theoria.Validation.DefeqCheck](Theoria.Validation.DefeqCheck.md): A Theoria-owned definitional-equality validation check.
  - [Theoria.Validation.IndexedMatchers](Theoria.Validation.IndexedMatchers.md): Validation helpers for explicit indexed matcher metadata packages.
  - [Theoria.Validation.InductiveCheck](Theoria.Validation.InductiveCheck.md): A Theoria-owned validation check for a built-in inductive specification.
  - [Theoria.Validation.Library](Theoria.Validation.Library.md): Validation checks owned by a Theoria library.
  - [Theoria.Validation.Report](Theoria.Validation.Report.md): Summary of a Theoria validation run.
  - [Theoria.Validation.SmallTerms](Theoria.Validation.SmallTerms.md): Deterministic small normalized-term checks owned by Theoria validation.
  - [Theoria.Validation.Terms](Theoria.Validation.Terms.md): Shared core terms used by Theoria validation checks.
  - [Theoria.Validation.TheoremModuleCheck](Theoria.Validation.TheoremModuleCheck.md): A validation check for a Theoria theorem module.

- Libraries
  - [Theoria.Library.Bool](Theoria.Library.Bool.md): Initial computational boolean declarations.
  - [Theoria.Library.Bool.Theorems](Theoria.Library.Bool.Theorems.md): Theorem corpus for `Theoria.Library.Bool`.
  - [Theoria.Library.Bool.Validation](Theoria.Library.Bool.Validation.md): Validation metadata for `Theoria.Library.Bool`.
  - [Theoria.Library.Equality.Theorems](Theoria.Library.Equality.Theorems.md): Theorem corpus for primitive propositional equality.
  - [Theoria.Library.Equality.Validation](Theoria.Library.Equality.Validation.md): Validation metadata for `Theoria.Library.Equality`.
  - [Theoria.Library.List](Theoria.Library.List.md): Initial polymorphic list declarations and primitive recursion.

  - [Theoria.Library.List.Theorems](Theoria.Library.List.Theorems.md): Theorem corpus for `Theoria.Library.List`.
  - [Theoria.Library.List.Validation](Theoria.Library.List.Validation.md): Validation metadata for `Theoria.Library.List`.
  - [Theoria.Library.Logic](Theoria.Library.Logic.md): Basic logical constants and checked definitions.
  - [Theoria.Library.Logic.Theorems](Theoria.Library.Logic.Theorems.md): Theorem corpus for `Theoria.Library.Logic`.
  - [Theoria.Library.Logic.Validation](Theoria.Library.Logic.Validation.md): Validation metadata for `Theoria.Library.Logic`.
  - [Theoria.Library.Nat](Theoria.Library.Nat.md): Initial natural number declarations and primitive recursion.

  - [Theoria.Library.Nat.Theorems](Theoria.Library.Nat.Theorems.md): Theorem corpus for `Theoria.Library.Nat`.
  - [Theoria.Library.Nat.Validation](Theoria.Library.Nat.Validation.md): Validation metadata for `Theoria.Library.Nat`.
  - [Theoria.Library.Vec](Theoria.Library.Vec.md): Length-indexed vectors.
  - [Theoria.Library.Vec.Theorems](Theoria.Library.Vec.Theorems.md): Theorem corpus for `Theoria.Library.Vec`.
  - [Theoria.Library.Vec.Validation](Theoria.Library.Vec.Validation.md): Validation metadata for `Theoria.Library.Vec`.

- Workflows
  - [Theoria.Prelude](Theoria.Prelude.md): The standard Theoria environment.
  - [Theoria.Theorem](Theoria.Theorem.md): A theorem accepted by the trusted kernel.

- Tooling
  - [Theoria.Lean.Encodable](Theoria.Lean.Encodable.md): Experimental/internal API for 0.2; subject to change before 0.3. Protocol for rendering Theoria structures as Lean oracle source.
  - [Theoria.Lean.Encode](Theoria.Lean.Encode.md): Experimental/internal API for 0.2; subject to change before 0.3.
  - [Theoria.Lean.Encode.Application](Theoria.Lean.Encode.Application.md): Experimental/internal API for 0.2; subject to change before 0.3. Specialized Lean encoders for application spines.
  - [Theoria.Lean.Mirror.Inductive](Theoria.Lean.Mirror.Inductive.md): Experimental/internal API for 0.2; subject to change before 0.3. Generates small Lean mirror declarations from Theoria inductive specs.
  - [Theoria.Lean.MirrorPrelude](Theoria.Lean.MirrorPrelude.md): Experimental/internal API for 0.2; subject to change before 0.3. Lean declarations that bridge Theoria primitives not rendered directly to Lean core.
  - [Theoria.Lean.Module](Theoria.Lean.Module.md): Experimental/internal API for 0.2; subject to change before 0.3. Builds Lean oracle source files from encoded checks.
  - [Theoria.Lean.Oracle](Theoria.Lean.Oracle.md): Experimental/internal API for 0.2; subject to change before 0.3. Runs generated Lean oracle files for contributor validation.

## Mix Tasks

- [mix theoria.check](Mix.Tasks.Theoria.Check.md): Checks Theoria's native validation corpus.
- [mix theoria.equations](Mix.Tasks.Theoria.Equations.md): Lists generated equation lemmas for definitions with stored equation metadata.

- [mix theoria.lean.check](Mix.Tasks.Theoria.Lean.Check.md): Generates Lean source from Theoria validation data and asks Lean to validate it.
- [mix theoria.simp](Mix.Tasks.Theoria.Simp.md): Runs small built-in simplification examples.

- [mix theoria.theorems](Mix.Tasks.Theoria.Theorems.md): Checks Theoria theorem modules against the standard prelude.

- [mix theoria.validate](Mix.Tasks.Theoria.Validate.md): Validates Theoria's native theorem, defeq, and inductive corpus.

