The substitution function of LaTTe is highly non-trivial, and well-tested although most bug found related to it at least indirectly.
Maybe NBE (normalization by evaluation) could be used for a safer substitution function.
(one drawback, though, is that NBE is difficult to debug because of the created closures)
The substitution function of LaTTe is highly non-trivial, and well-tested although most bug found related to it at least indirectly.
Maybe NBE (normalization by evaluation) could be used for a safer substitution function.
(one drawback, though, is that NBE is difficult to debug because of the created closures)