blob: aa883f5e7095b4caf6e713276de6c7a4deab7ec0 (
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.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.
|
