diff options
Diffstat (limited to 'src/Compilers/Z/OpInversion.v')
| -rw-r--r-- | src/Compilers/Z/OpInversion.v | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/Compilers/Z/OpInversion.v b/src/Compilers/Z/OpInversion.v deleted file mode 100644 index c27f51aee..000000000 --- a/src/Compilers/Z/OpInversion.v +++ /dev/null @@ -1,29 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.Z.TypeInversion. -Require Import Crypto.Compilers.Z.Syntax. - -Ltac invert_one_op e := - preinvert_one_type e; - intros ? e; - destruct e; - try exact I. - -Ltac invert_op_step := - match goal with - | [ e : op _ (Tbase _) |- _ ] => invert_one_op e - | [ e : op _ (Prod _ _) |- _ ] => invert_one_op e - | [ e : op _ Unit |- _ ] => invert_one_op e - end. - -Ltac invert_op := repeat invert_op_step. - -Ltac invert_match_op_step := - match goal with - | [ |- context[match ?e with OpConst _ _ => _ | _ => _ end] ] - => invert_one_op e - | [ H : context[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ] - => invert_one_op e - end. - -Ltac invert_match_op := repeat invert_match_op_step. |