blob: 281bee6ab63de726c4862378d59e26b8e7ee924a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.InlineConstAndOpByRewriteWf.
Require Import Crypto.Compilers.ZExtended.Syntax.
Require Import Crypto.Compilers.ZExtended.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.
|
