Inductive specifications

Theoria describes primitive inductive families with data structs, then admits the resulting declarations through the kernel. The DSL and spec builders are untrusted conveniences; Theoria.Kernel.add_inductive/2 is the admission boundary.

A small Bool-like family can be written with constructors only and completed with generated eliminators:

alias Theoria.{Env, Inductive, Kernel}
alias Theoria.Inductive.Spec

import Theoria.DSL

spec =
  :Switch
  |> Spec.new(term(do: sort(1)) |> elab!())
  |> Spec.constructor(:on, term(do: const(:Switch)) |> elab!())
  |> Spec.constructor(:off, term(do: const(:Switch)) |> elab!())

{:ok, spec} = Inductive.complete(spec)
{:ok, env} = Kernel.add_inductive(Env.new(), spec)

You can inspect the shape and declaration plan before admission:

Inductive.shape(spec)
#=> :bool_like

shape = Inductive.classify(spec)
shape.constructors.first.name
#=> :on

{:ok, report} = Inductive.report(spec)
report.declarations
#=> [:Switch, :on, :off, :switch_rec, :switch_ind]

For parameterized families, declare named parameters explicitly. The validator checks that constructor result arguments preserve those parameters:

u = Theoria.Level.param(:u)

type =
  term do
    forall :a, sort(^u) do
      sort(^u)
    end
  end
  |> elab!()

spec =
  :List
  |> Spec.new(type, universe_params: [:u, :v])
  |> Spec.parameter(:a, term(do: sort(^u)) |> elab!())

Indexed families can declare named indices. The current checker validates result arity, parameter preservation, and scopedness of constructor argument/index terms. Theoria.Inductive.Generate.indexed_eliminators/1 can synthesize indexed induction declarations with Theoria.Env.Recursor metadata and validated Theoria.Env.RecursorRule entries. These rules record constructor field counts, RHS templates, and index patterns; normalization uses them when an iota marker is present and refuses to reduce when explicit recursor indices do not match the selected constructor rule pattern. Environment-backed admission also requires dependencies to be present. Theoria.Library.Vec packages this fragment as the standard length-indexed vector library. Custom Vec-like specs must be checked in an environment that already contains Nat, zero, and succ.

u = Theoria.Level.param(:u)

vec_type =
  term do
    forall :a, sort(^u) do
      nat() ~> sort(^u)
    end
  end
  |> elab!()

spec =
  :Vec
  |> Spec.new(vec_type, universe_params: [:u])
  |> Spec.parameter(:a, term(do: sort(^u)) |> elab!())
  |> Spec.index(:n, term(do: nat()) |> elab!())

The built-in Bool, Nat, and List libraries use Theoria.Inductive.Generate.eliminators/1 through this same path. Their constructor targets are decomposed with Theoria.Inductive.Constructor.result/2; simple non-indexed recursor/induction types and generic reduction metadata are derived from that decomposition. Theoria.Inductive.Generate.capabilities/1 reports whether a spec is currently supported by the reducing simple-eliminator generator; indexed specs use indexed_eliminators/1 separately. Generated declarations also carry Lean-style environment metadata (Theoria.Env.Inductive, Theoria.Env.Constructor, Theoria.Env.Recursor, and Theoria.Env.RecursorRule) so tools can distinguish type formers, constructors, and recursors without relying on naming conventions. Generated eliminators use Theoria.Env.Reduction.Iota as a primitive-reduction marker; normalization selects and instantiates the matching Theoria.Env.RecursorRule RHS.