Modules
An Elixir-native proof/spec kernel inspired by Lean's trusted-kernel design.
Typing context for bound variables.
Small Elixir DSL for constructing named Theoria syntax terms.
Converts named Theoria.Syntax terms to de Bruijn-indexed Theoria.Term terms.
Kernel environment containing checked constants and definitions.
A checked constant or definition in a kernel environment.
Lean-style metadata for an admitted inductive constructor.
Lean-style metadata for an admitted inductive type former.
Environment metadata for a generated matcher declaration.
Lean-style metadata for an admitted inductive recursor.
Lean-style iota-reduction rule metadata for a recursor constructor case.
Primitive reduction metadata attached to environment declarations.
Marks a recursor declaration as using constructor iota-reduction rules.
Untrusted helpers for building equality transport terms.
Experimental/internal API for 0.2; subject to change before 0.3.
Experimental/internal API for 0.2; subject to change before 0.3. Internal constructor-specific branch descriptors for equation compilation.
Experimental/internal API for 0.2; subject to change before 0.3. Schematic equation case template used by schema generation.
Experimental/internal API for 0.2; subject to change before 0.3. A constructor equation clause.
Experimental/internal API for 0.2; subject to change before 0.3. Result of compiling constructor equations, including generated metadata.
Experimental/internal API for 0.2; subject to change before 0.3. Internal constructor-equation compiler for the initial Bool/Nat/List fragment.
Experimental/internal API for 0.2; subject to change before 0.3. Internal named values available while materializing an equation branch body.
Experimental/internal API for 0.2; subject to change before 0.3. Small internal helpers for building core lambda definitions.
Experimental/internal API for 0.2; subject to change before 0.3. Complete metadata package for a compiled equation definition.
Experimental/internal API for 0.2; subject to change before 0.3. Lookup helpers for generated equation theorem metadata.
Experimental/internal API for 0.2; subject to change before 0.3. Typed registry helpers for generated equation and matcher metadata.
In-memory registry snapshot for generated equation metadata.
Experimental/internal API for 0.2; subject to change before 0.3. Minimal descriptor for fixed parameters of compiled equation definitions.
Structured identity for generated equation artifacts.
Experimental/internal API for 0.2; subject to change before 0.3. Lean-inspired metadata for a compiled equation definition.
Experimental/internal API for 0.2; subject to change before 0.3. Metadata for an equation lemma generated from compiled equations.
Experimental/internal API for 0.2; subject to change before 0.3. Internal descriptor-driven matcher generation metadata.
Descriptor for one matcher alternative.
Normalized constructor field shape for matcher descriptors.
Experimental/internal API for 0.2; subject to change before 0.3. Lookup helpers for generated matcher equation metadata.
Experimental/internal API for 0.2; subject to change before 0.3. Metadata for an equation generated for a matcher alternative.
Experimental/internal API for 0.2; subject to change before 0.3. Coherent package for indexed matcher equation metadata.
Experimental/internal API for 0.2; subject to change before 0.3. Realization planning for indexed matcher equations.
Realization plan for one indexed matcher equation.
Realization plan for an indexed matcher equation package.
Experimental/internal API for indexed Vec matcher metadata packages.
Experimental/internal API for 0.2; subject to change before 0.3. Small Theoria-side mirror of Lean matcher metadata.
Metadata for one matcher alternative.
Metadata for one matcher discriminant.
Experimental/internal API for 0.2; subject to change before 0.3. Checked declaration package for a generated matcher.
Experimental/internal API for 0.2; subject to change before 0.3. Statement planning for matcher equations.
Dispatches indexed matcher equation statement planning to family-specific planners.
Internal binder frame for matcher equation statement planning.
Shared helpers for indexed matcher statement planning.
Internal indexed Vec statement planner for matcher equations.
Experimental/internal API for 0.2; subject to change before 0.3. Internal builder for checked matcher declaration types and bodies for supported fragments.
Matcher branch type descriptor.
Planned matcher declaration shape derived from a matcher descriptor.
Experimental/internal API for 0.2; subject to change before 0.3. Equation compiler patterns.
A constructor pattern with subpatterns.
A variable pattern.
A wildcard pattern.
A kernel-checked generated equation artifact that is not necessarily installed as a theorem.
Experimental/internal API for 0.2; subject to change before 0.3. Internal raw recursor application builders used by the equation compiler.
Experimental/internal API for 0.2; subject to change before 0.3. Internal recursor-derived shape metadata for matcher descriptors.
Recursor rule shape used by matcher descriptor generation.
Constructor field shape in a recursor rule.
Experimental/internal API for 0.2; subject to change before 0.3. Schema metadata for generating equation lemmas from compiled definitions.
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.
One schematic equation theorem generated for a compiled definition.
Experimental/internal API for 0.2; subject to change before 0.3. Telescope summary for compiler-owned equation metadata generation.
Experimental/internal API for 0.2; subject to change before 0.3. Validation for constructor-equation clauses.
Kernel error returned when a term cannot be checked.
Validation helpers for inductive specifications.
Staged admission pipeline for inductive specifications.
Constructor declaration in an inductive specification.
Decomposed constructor target and binders.
Generated declaration plan for an inductive specification.
Generators for declarations derived from inductive specs.
Named index of an inductive family.
Named parameter of an inductive family.
Recursor or induction principle declaration in an inductive specification.
Summary of an inductive declaration plan.
Structured classification of supported inductive shapes.
Structured description of an inductive family.
The trusted type-checking kernel.
Validation for trusted recursor iota rules.
Dependency and trust summary for an environment declaration.
Experimental/internal API for 0.2; subject to change before 0.3. Protocol for rendering Theoria structures as Lean oracle source.
Experimental/internal API for 0.2; subject to change before 0.3.
Experimental/internal API for 0.2; subject to change before 0.3. Specialized Lean encoders for application spines.
Experimental/internal API for 0.2; subject to change before 0.3. Generates small Lean mirror declarations from Theoria inductive specs.
Experimental/internal API for 0.2; subject to change before 0.3. Lean declarations that bridge Theoria primitives not rendered directly to Lean core.
Experimental/internal API for 0.2; subject to change before 0.3. Builds Lean oracle source files from encoded checks.
Experimental/internal API for 0.2; subject to change before 0.3. Runs generated Lean oracle files for contributor validation.
Universe levels.
Universe-level ordering constraint.
Maximum of two universe levels.
A universe level parameter.
Small solver for universe-level ordering constraints.
Successor universe level.
The zero universe level.
Initial computational boolean declarations.
Theorem corpus for Theoria.Library.Bool.
Validation metadata for Theoria.Library.Bool.
Theorem corpus for primitive propositional equality.
Validation metadata for Theoria.Library.Equality.
Initial polymorphic list declarations and primitive recursion.
Theorem corpus for Theoria.Library.List.
Validation metadata for Theoria.Library.List.
Basic logical constants and checked definitions.
Theorem corpus for Theoria.Library.Logic.
Validation metadata for Theoria.Library.Logic.
Initial natural number declarations and primitive recursion.
Theorem corpus for Theoria.Library.Nat.
Validation metadata for Theoria.Library.Nat.
Length-indexed vectors.
Theorem corpus for Theoria.Library.Vec.
Validation metadata for Theoria.Library.Vec.
Normalization and definitional equality for core terms.
Shared fuel budget for normalization.
Primitive weak-head reductions for declarations with iota metadata.
The standard Theoria environment.
Human-readable rendering for Theoria values.
Experimental/internal API for 0.2; subject to change before 0.3. Untrusted structural rewrite helpers over core terms.
Experimental/internal API for 0.2; subject to change before 0.3. A tiny untrusted rewrite-rule database.
Experimental/internal API for 0.2; subject to change before 0.3. Untrusted first-order matching for schematic rewrite rules.
Experimental/internal API for 0.2; subject to change before 0.3. A theorem-like rewrite rule over a core equality term.
Experimental/internal API for 0.2; subject to change before 0.3. Tiny untrusted simplification groundwork backed by generated equation rules.
Experimental/internal API for 0.2; subject to change before 0.3. Untrusted simplifier database with rule priorities.
Experimental/internal API for 0.2; subject to change before 0.3. Simplifier rule metadata layered over untrusted rewrite rules.
Experimental/internal API for 0.2; subject to change before 0.3. One simplifier rewrite step for tracing and debugging.
Named surface terms for building Theoria core terms.
Function application.
A named environment constant.
Named-syntax propositional equality.
Named-syntax equality recursor.
Dependent function type with a named binder.
Lambda abstraction with a named binder.
Local definition with a named binder.
Named-syntax reflexivity proof.
A named-syntax universe level.
A named bound variable.
Core terms for Theoria's trusted kernel.
Function application.
Helpers for application terms.
A bound variable represented by a de Bruijn index.
A named environment constant.
Propositional equality over a type.
Primitive equality recursor.
Dependent function type. Non-dependent functions are encoded as forall types.
Lambda abstraction.
Local definition.
Reflexivity proof for propositional equality.
A universe level, written Type n in the surface language.
A theorem accepted by the trusted kernel.
Runs Theoria-owned validation corpora.
Protocol for running Theoria validation checks.
Core calculus validation checks.
Theoria-owned validation corpus consumed by local checks and external oracles.
A Theoria-owned definitional-equality validation check.
Validation helpers for explicit indexed matcher metadata packages.
A Theoria-owned validation check for a built-in inductive specification.
Validation checks owned by a Theoria library.
Summary of a Theoria validation run.
Deterministic small normalized-term checks owned by Theoria validation.
Shared core terms used by Theoria validation checks.
A validation check for a Theoria theorem module.
Mix Tasks
Checks Theoria's native validation corpus.
Lists generated equation lemmas for definitions with stored equation metadata.
Generates Lean source from Theoria validation data and asks Lean to validate it.
Runs small built-in simplification examples.
Checks Theoria theorem modules against the standard prelude.
Validates Theoria's native theorem, defeq, and inductive corpus.