blob: e67442c7118a7684c75c50a311a8b29b79c19499 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.InlineConstAndOpByRewriteInterp.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.InlineConstAndOpByRewrite.
Module Export Rewrite.
Definition InterpInlineConstAndOp {t} (e : Expr t)
: forall x, Interp (InlineConstAndOp e) x = Interp e x
:= @InterpInlineConstAndOp _ _ _ _ _ t e Syntax.Util.make_const_correct.
Hint Rewrite @InterpInlineConstAndOp : reflective_interp.
End Rewrite.
|
