diff options
Diffstat (limited to 'src/Compilers/Z/InlineConstAndOpByRewriteWf.v')
| -rw-r--r-- | src/Compilers/Z/InlineConstAndOpByRewriteWf.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Compilers/Z/InlineConstAndOpByRewriteWf.v b/src/Compilers/Z/InlineConstAndOpByRewriteWf.v new file mode 100644 index 000000000..aa883f5e7 --- /dev/null +++ b/src/Compilers/Z/InlineConstAndOpByRewriteWf.v @@ -0,0 +1,13 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.InlineConstAndOpByRewriteWf. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.InlineConstAndOpByRewrite. + +Module Export Rewrite. + Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e) + : Wf (InlineConstAndOp e) + := @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf. + + Hint Resolve Wf_InlineConstAndOp : wf. +End Rewrite. |