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.
Term quotation implementation for Theoria.DSL.
Prelude-specific term quote sugar.
Theorem macro support for Theoria.DSL.
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.
Builds kernel-checked equality artifacts for rewrite/simp traces.
Proof term and strategy selected for an equality chain.
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.
Shared declaration-admission checks used by trusted kernel entrypoints.
Experimental generated-artifact replay summary for Theoria 0.5 assurance reports.
Experimental generated-artifact replay skip entry for Theoria 0.5 assurance reports.
Trusted-adjacent admission checks for constants and axioms.
Curated kernel terms for production/reference differential checks.
Kernel assurance coverage summary.
Trusted-adjacent admission checks for transparent definitions.
Production/reference kernel differential checks.
Structured options for kernel differential assurance runs.
Summary of kernel differential checks.
Experimental assurance-report timing metadata for Theoria 0.5.
Experimental trust-boundary explanation data for Theoria 0.5 reports.
A generated closed term paired with its expected type for assurance tests.
Diagnostic payload for a generated-term differential failure.
Structured generated-term differential coverage summary.
Experimental typed term generators for kernel/reference differential assurance.
Trusted-adjacent admission boundary for inductive declarations.
Trusted-adjacent admission checks for matcher declarations.
Structured proof-strategy count summary for generated artifacts.
Validation for trusted recursor iota rules.
Slow, explicit reference checker for the first Theoria kernel fragment.
Reference normalization for kernel differential assurance.
Reference primitive reductions for recursor iota metadata.
Reference replay of checked environment declarations.
Reference environment replay summary.
Elixir-authored metadata for Theoria's trusted kernel fragment.
Trusted-adjacent admission checks for opaque theorem declarations.
Experimental theorem-module assurance summary for Theoria 0.5 reports.
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.
Explicit collection of universe-level ordering constraints.
Maximum of two universe levels.
A universe level parameter.
Small solver for universe-level ordering constraints.
Structured explanation for one universe-constraint solver result.
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.
Proof construction helpers for structural rewrite steps.
Experimental boundary helper for binder-path proof lifting attempts.
Experimental proof-lifting capability matrix for Theoria 0.6.
Experimental proof-lifting capability descriptor for Theoria 0.5.
Experimental proof capability matrix entry for Theoria 0.5.
Experimental EqRec-path proof lifting helpers.
Experimental proof-diagnostic result for Theoria 0.5 rewrite and simp steps.
Experimental/internal API for 0.2; subject to change before 0.3. A theorem-like rewrite rule over a core equality term.
One structural rewrite application with the matched path and optional proof data.
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.
Result of repeated simplification, including optional proof artifact data.
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.
Runs production/reference kernel differential checks.
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.