blob: 46e5064e94ca684c8c219d5a4dc2b6afa1b15e5d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
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 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 @InterpInlineConstAndOpp @InterpInlineConst using solve_wf_side_condition : reflective_interp.
|
