Shared helpers for indexed matcher statement planning.
Summary
Functions
Applies arguments left-to-right to a function term.
Collects a forall telescope into {name, domain} pairs.
Returns references to named binders in order.
Returns the binder telescope common to indexed matcher equations.
Derives current statement levels from parameter sorts.
Functions
@spec apply_args(Theoria.Term.t(), [Theoria.Term.t()]) :: Theoria.Term.t()
Applies arguments left-to-right to a function term.
@spec collect_foralls(Theoria.Term.t()) :: [{atom(), Theoria.Term.t()}]
Collects a forall telescope into {name, domain} pairs.
@spec refs_for_names(Theoria.Equation.Matcher.Statement.Frame.t(), [atom()]) :: {:ok, [Theoria.Term.t()]} | {:error, term()}
Returns references to named binders in order.
@spec statement_binders(term()) :: [{atom(), Theoria.Term.t()}]
Returns the binder telescope common to indexed matcher equations.
Derives current statement levels from parameter sorts.