diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-13 23:12:25 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-13 23:12:25 -0400 |
| commit | 2b5f90c8dcaf2475dc066a593976372729460b40 (patch) | |
| tree | 53d3f3554cec70c714e00a7e2617f44dffa5daa8 /src | |
| parent | 78f4e1c603e50877f291cc0e1cee4a772c6bcc09 (diff) | |
Add rewrite_eta_match_base_type_impl
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 084786529..ceff9283e 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -308,3 +308,11 @@ Lemma eta_match_base_type_impl P1 P2 PZ T | TWord _ => fun _ => PZ end = fun _ => PZ. Proof. destruct T; reflexivity. Qed. +Ltac rewrite_eta_match_base_type_impl_step := + match goal with + | [ H : context[match ?T as T' in base_type return (@?P1 T' -> ?P2) with TZ => _ | _ => _ end] |- _ ] + => rewrite (@eta_match_base_type_arr P1 P2) in H + | [ |- context[match ?T as T' in base_type return (@?P1 T' -> ?P2) with TZ => _ | _ => _ end] ] + => rewrite (@eta_match_base_type_arr P1 P2) + end. +Ltac rewrite_eta_match_base_type_impl := repeat rewrite_eta_match_base_type_impl_step. |