blob: b7726987bde731414e333ea2dffac25eafd90a16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.InlineWf.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Inline.
Definition Wf_InlineConstAndOpp {t} (e : Expr t) (Hwf : Wf e)
: Wf (InlineConstAndOpp e)
:= @Wf_InlineConst _ _ _ t e Hwf.
Definition Wf_InlineConst {t} (e : Expr t) (Hwf : Wf e)
: Wf (InlineConst e)
:= @Wf_InlineConst _ _ _ t e Hwf.
Hint Resolve Wf_InlineConstAndOpp Wf_InlineConst : wf.
|
