Experimental/internal API for 0.2; subject to change before 0.3. Internal raw recursor application builders used by the equation compiler.
Summary
Functions
Builds a Bool recursor application from the two constructor equations.
Builds a recursor application from a recursor name and positional arguments.
Builds a List recursor application from nil/cons equations.
Builds a Nat recursor application from zero/succ equations.
Builds a Vec recursor application from nil/cons equations.
Functions
@spec bool_rec(Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t()) :: Theoria.Term.t()
Builds a Bool recursor application from the two constructor equations.
@spec build(atom(), [Theoria.Term.t()]) :: {:ok, Theoria.Term.t()} | {:error, term()}
Builds a recursor application from a recursor name and positional arguments.
@spec list_rec( Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), [Theoria.Level.t() | non_neg_integer()] ) :: Theoria.Term.t()
Builds a List recursor application from nil/cons equations.
@spec nat_rec(Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t()) :: Theoria.Term.t()
Builds a Nat recursor application from zero/succ equations.
@spec vec_ind( Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), [Theoria.Level.t() | non_neg_integer()] ) :: Theoria.Term.t()
Builds a Vec recursor application from nil/cons equations.