aboutsummaryrefslogtreecommitdiff
path: root/src/Util/SideConditions/ReductionPackages.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-10-14 17:17:10 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-10-14 17:17:10 -0400
commit4b8ff5478b367cce44c87d5e3ecd94ff37593d57 (patch)
tree57f1d09e3ce948e056708133df2813d9f0510e1f /src/Util/SideConditions/ReductionPackages.v
parent3a69ac966dbd03e1f5192b68b6328f2028b02e24 (diff)
Add placeholder rewrite rules for rewriting after bounds
Currently, there aren't any interesting rewrite rules in the lists, but this allows us to move rewrite rules that depend on cast behavior to after bounds analysis. Unfortunately, it takes a lot of time to build from Rewriter.v to the standalone binaries, so it'll probably make sense to inline some stuff for more rapid development. Note that we also now have a tactic that does all of the evaluation for rewrite rules (assuming the right [Arguments] commands have been issued).
Diffstat (limited to 'src/Util/SideConditions/ReductionPackages.v')
0 files changed, 0 insertions, 0 deletions