blob: 3f1a83f3d0deb6ac38f518b82fff213e02daced0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.InlineConstAndOpInterp.
Require Import Crypto.Compilers.ZExtended.Syntax.
Require Import Crypto.Compilers.ZExtended.InlineConstAndOp.
Definition InterpInlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
: forall x, Interp (InlineConstAndOp e) x = Interp e x.
Proof.
refine (@InterpInlineConstAndOp _ _ _ _ _ t e Hwf _).
clear; abstract (intros []; intros; reflexivity).
Defined.
Hint Rewrite @InterpInlineConstAndOp using solve_wf_side_condition : reflective_interp.
|
