diff options
Diffstat (limited to 'src/Compilers/Z/InlineInterp.v')
| -rw-r--r-- | src/Compilers/Z/InlineInterp.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Compilers/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v index b0cd0b8df..46e5064e9 100644 --- a/src/Compilers/Z/InlineInterp.v +++ b/src/Compilers/Z/InlineInterp.v @@ -4,8 +4,12 @@ Require Import Crypto.Compilers.InlineInterp. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Inline. +Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e) + : forall x, Interp interp_op (InlineConstAndOpp e) x = Interp interp_op e x + := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf. + 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_wf_side_condition : reflective_interp. +Hint Rewrite @InterpInlineConstAndOpp @InterpInlineConst using solve_wf_side_condition : reflective_interp. |