blob: aa0f41d077b6ffba7a8e7a1720412878470d407a (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.InlineConstAndOpWf.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.InlineConstAndOp.
Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
: Wf (InlineConstAndOp e)
:= @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf.
Hint Resolve Wf_InlineConstAndOp : wf.
|
