Shared core terms used by Theoria validation checks.
Summary
Functions
List cons branch that increments a Nat accumulator.
Nat successor branch for non-dependent recursors returning Nat.
Vec motive returning Nat for each index/vector pair.
Vec cons branch that increments the induction hypothesis.
Functions
@spec list_succ_case(Theoria.Term.t()) :: Theoria.Term.t()
List cons branch that increments a Nat accumulator.
@spec nat_succ_case() :: Theoria.Term.t()
Nat successor branch for non-dependent recursors returning Nat.
@spec vec_nat_motive() :: Theoria.Term.t()
Vec motive returning Nat for each index/vector pair.
@spec vec_succ_case() :: Theoria.Term.t()
Vec cons branch that increments the induction hypothesis.