Theoria.Equation (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3.

Internal constructor-equation compiler facade.

Theoria.Equation supports the current Bool/Nat/List recursor fragment. It is not yet a public pattern-matching language: callers still construct core terms and explicit clauses, while the compiler handles coverage, pattern-shape validation, and recursor assembly.

Summary

Functions

bool_rec(motive, on_true, on_false, major)

See Theoria.Equation.Recursor.Application.bool_rec/4.

compile(kind, motive, clauses, major)

See Theoria.Equation.Compiler.compile/4.

compile_bool(motive, clauses, major)

See Theoria.Equation.Compiler.compile_bool/3.

compile_bool(motive, clauses, major, context)

See Theoria.Equation.Compiler.compile_bool/4.

compile_definition(kind, signature, motive, clauses, major, opts)

See Theoria.Equation.Compiler.compile_definition/6.

compile_list(element_type, motive, clauses, major)

See Theoria.Equation.Compiler.compile_list/4.

compile_list(element_type, motive, clauses, major, levels)

See Theoria.Equation.Compiler.compile_list/5.

compile_nat(motive, clauses, major)

See Theoria.Equation.Compiler.compile_nat/3.

list_rec(element_type, motive, nil_case, cons_case, major)

See Theoria.Equation.Recursor.Application.list_rec/5.

list_rec(element_type, motive, nil_case, cons_case, major, levels)

See Theoria.Equation.Recursor.Application.list_rec/6.

nat_rec(motive, zero_case, succ_case, major)

See Theoria.Equation.Recursor.Application.nat_rec/4.

Functions

bool_rec(motive, on_true, on_false, major)

See Theoria.Equation.Recursor.Application.bool_rec/4.

compile(kind, motive, clauses, major)

See Theoria.Equation.Compiler.compile/4.

compile_bool(motive, clauses, major)

See Theoria.Equation.Compiler.compile_bool/3.

compile_bool(motive, clauses, major, context)

See Theoria.Equation.Compiler.compile_bool/4.

compile_definition(kind, signature, motive, clauses, major, opts)

See Theoria.Equation.Compiler.compile_definition/6.

compile_list(element_type, motive, clauses, major)

See Theoria.Equation.Compiler.compile_list/4.

compile_list(element_type, motive, clauses, major, levels)

See Theoria.Equation.Compiler.compile_list/5.

compile_nat(motive, clauses, major)

See Theoria.Equation.Compiler.compile_nat/3.

list_rec(element_type, motive, nil_case, cons_case, major)

See Theoria.Equation.Recursor.Application.list_rec/5.

list_rec(element_type, motive, nil_case, cons_case, major, levels)

See Theoria.Equation.Recursor.Application.list_rec/6.

nat_rec(motive, zero_case, succ_case, major)

See Theoria.Equation.Recursor.Application.nat_rec/4.