Experimental/internal API for 0.2; subject to change before 0.3. Untrusted first-order matching for schematic rewrite rules.
Summary
Functions
Instantiates low de Bruijn variables in a template using a substitution.
Matches pattern against term, treating low de Bruijn variables as metavariables.
Types
@type substitution() :: %{required(non_neg_integer()) => Theoria.Term.t()}
Functions
@spec instantiate(Theoria.Term.t(), substitution()) :: Theoria.Term.t()
Instantiates low de Bruijn variables in a template using a substitution.
@spec match(Theoria.Term.t(), Theoria.Term.t(), non_neg_integer()) :: {:ok, substitution()} | :error
Matches pattern against term, treating low de Bruijn variables as metavariables.