blob: b0cd0b8df11c35e6cd14d29265331313ae6ae374 (
plain)
1
2
3
4
5
6
7
8
9
10
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_wf_side_condition : reflective_interp.
|
