• Robbert Krebbers's avatar
    Implement substitution by reification. · dd543f95
    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
one_shot.v 4.02 KB