InPlace
An implementation of several strongly-normalizing string rewriting systems
Relog Flavor
a=Int;List<a>
List<Int>
A<b,C<d>>=A<Int,C<Bool>>;R<b>
R<Int>
A<b,c>:=R<c>;A<B,C>
R<C>
$$apply \ \ \frac{unify(f,fx)⊢r}{f⇻r⊢reify(apply(r))}$$
An implementation of several strongly-normalizing string rewriting systems
a=Int;List<a>
List<Int>
A<b,C<d>>=A<Int,C<Bool>>;R<b>
R<Int>
A<b,c>:=R<c>;A<B,C>
R<C>
$$apply \ \ \frac{unify(f,fx)⊢r}{f⇻r⊢reify(apply(r))}$$