blob: 3ce24e2378bdb992646e7e63602586dee6d62436 (
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.ZExtended.Syntax.
Require Import Crypto.Compilers.ZExtended.InlineConstAndOp.
Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
: Wf (InlineConstAndOp e)
:= @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf.
Hint Resolve Wf_InlineConstAndOp : wf.
|
