diff options
Diffstat (limited to 'src/Compilers/Z/InlineWf.v')
| -rw-r--r-- | src/Compilers/Z/InlineWf.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Compilers/Z/InlineWf.v b/src/Compilers/Z/InlineWf.v index 32b84aa1f..d6b846460 100644 --- a/src/Compilers/Z/InlineWf.v +++ b/src/Compilers/Z/InlineWf.v @@ -4,8 +4,12 @@ Require Import Crypto.Compilers.InlineWf. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Inline. +Definition Wf_InlineConstAndOpp {t} (e : Expr base_type op t) (Hwf : Wf e) + : Wf (InlineConstAndOpp e) + := @Wf_InlineConst _ _ _ t e Hwf. + Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e) : Wf (InlineConst e) := @Wf_InlineConst _ _ _ t e Hwf. -Hint Resolve Wf_InlineConst : wf. +Hint Resolve Wf_InlineConstAndOpp Wf_InlineConst : wf. |