• 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
Name
Last commit
Last update
..
lib Loading commit data...
derived.v Loading commit data...
heap.v Loading commit data...
lang.v Loading commit data...
lifting.v Loading commit data...
notation.v Loading commit data...
proofmode.v Loading commit data...
substitution.v Loading commit data...
tactics.v Loading commit data...
wp_tactics.v Loading commit data...