diff options
Diffstat (limited to 'src/Compilers/Named/ExprInversion.v')
| -rw-r--r-- | src/Compilers/Named/ExprInversion.v | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/src/Compilers/Named/ExprInversion.v b/src/Compilers/Named/ExprInversion.v deleted file mode 100644 index 783341f26..000000000 --- a/src/Compilers/Named/ExprInversion.v +++ /dev/null @@ -1,21 +0,0 @@ -Require Import Crypto.Compilers.TypeInversion. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. - -Module Export Named. - Ltac invert_one_expr e := - preinvert_one_type e; - intros ? e; - destruct e; - try exact I. - - Ltac invert_expr_step := - match goal with - | [ e : Named.exprf _ _ _ (Tbase _) |- _ ] => invert_one_expr e - | [ e : Named.exprf _ _ _ (Prod _ _) |- _ ] => invert_one_expr e - | [ e : Named.exprf _ _ _ Unit |- _ ] => invert_one_expr e - | [ e : Named.expr _ _ _ (Arrow _ _) |- _ ] => invert_one_expr e - end. - - Ltac invert_expr := repeat invert_expr_step. -End Named. |