diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-06 14:44:32 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-06 14:44:32 -0400 |
| commit | 8704021b9cd840b9ac0c304c0d767cfde2408b22 (patch) | |
| tree | d69634cd82a2701fcbac0b1a8cae7b6458115ea0 /src/BoundedArithmetic/Interface.v | |
| parent | 09a9310b877c5032146a6e73b59fcef9bda71e5e (diff) | |
Add more bounded assembly lemmas
Diffstat (limited to 'src/BoundedArithmetic/Interface.v')
| -rw-r--r-- | src/BoundedArithmetic/Interface.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/BoundedArithmetic/Interface.v b/src/BoundedArithmetic/Interface.v index 0550aeca5..4a671eb4c 100644 --- a/src/BoundedArithmetic/Interface.v +++ b/src/BoundedArithmetic/Interface.v @@ -37,6 +37,8 @@ Ltac push_decode_step := => tc_rewrite (decode_tag) (@decode n W decoder w) -> | [ |- context[match @fst ?A ?B ?x with true => 1 | false => 0 end] ] => tc_rewrite (decode_tag) (match @fst A B x with true => 1 | false => 0 end) -> + | [ |- context[@fst bool ?B ?x] ] + => tc_rewrite (decode_tag) (@fst bool B x) -> end. Ltac push_decode := repeat push_decode_step. Ltac pull_decode_step := |