blob: 783341f2627ac0dafb84418cdbc9a5adf4aa4fab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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.
|
