blob: 64d5263a70c63b3fd728f1a93260029f2959ad40 (
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.InlineConstAndOpByRewriteInterp.
Require Import Crypto.Compilers.ZExtended.Syntax.
Require Import Crypto.Compilers.ZExtended.InlineConstAndOpByRewrite.
Module Export Rewrite.
Lemma InterpInlineConstAndOp {t} (e : Expr t)
: forall x, Interp (InlineConstAndOp e) x = Interp e x.
Proof.
refine (@InterpInlineConstAndOp _ _ _ _ _ t e _).
clear; abstract (intros []; intros; reflexivity).
Defined.
Hint Rewrite @InterpInlineConstAndOp : reflective_interp.
End Rewrite.
|
