-
Robbert Krebbers authored
We reify to a representation of expressions that includes an explicit constructor for closed terms. Substitution can then be implemented as the identify, which enables us to perform it using computation.
dd543f95
We reify to a representation of expressions that includes an explicit constructor for closed terms. Substitution can then be implemented as the identify, which enables us to perform it using computation.