diff options
author | Jason Gross <jgross@mit.edu> | 2018-10-30 19:24:29 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-10-30 19:24:29 -0400 |
commit | 9f4911d5a10d06b2a78262c0ba81a1540570c56c (patch) | |
tree | be70db0946ded2bfb39e288a94e42e0fd93bf5fa /CONTRIBUTORS | |
parent | 47d73a9f76ed16ec2ca719f60d717ec9e16eef86 (diff) |
Refactor/generalize some pipeline definitions/proofs
When we do rewriting after casts, we will need to do extra passes of DCE
and subst01 to fully reduce things, so we generalize some of the interp
proofs over cast behavior.
For ease of rewriting, we make [ident.interp] an alias (notation) for
[ident.gen_interp], rather than a [Definition].
We also factor out the rewriting wrapper inside the pipeline module into
its own definition.
Diffstat (limited to 'CONTRIBUTORS')
0 files changed, 0 insertions, 0 deletions