diff options
Diffstat (limited to 'src/Compilers/Z/InlineInterp.v')
| -rw-r--r-- | src/Compilers/Z/InlineInterp.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Compilers/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v new file mode 100644 index 000000000..c02197331 --- /dev/null +++ b/src/Compilers/Z/InlineInterp.v @@ -0,0 +1,11 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.InlineInterp. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.Inline. + +Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e) + : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x + := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf. + +Hint Rewrite @InterpInlineConst using solve [ eassumption | eauto with wf ] : reflective_interp. |