diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-13 23:11:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-13 23:11:17 -0400 |
| commit | 78f4e1c603e50877f291cc0e1cee4a772c6bcc09 (patch) | |
| tree | 2f626f8cf9e76173def1af5edf7d23fced096f5a /src/Compilers/Z/Syntax | |
| parent | 805ef6e2c439544eabc1c54d5901050d0f6e934b (diff) | |
Add eta_match_base_type_impl
Diffstat (limited to 'src/Compilers/Z/Syntax')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 41b0e33be..084786529 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -301,3 +301,10 @@ Proof. induction x, y; simpl; auto. rewrite !Nat.leb_le; omega. Qed. + +Lemma eta_match_base_type_impl P1 P2 PZ T + : match T as T return P1 T -> P2 with + | TZ => fun _ => PZ + | TWord _ => fun _ => PZ + end = fun _ => PZ. +Proof. destruct T; reflexivity. Qed. |