diff options
Diffstat (limited to 'src/Compilers/Z/Inline.v')
| -rw-r--r-- | src/Compilers/Z/Inline.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v index 8a8bea98b..df46c0ecf 100644 --- a/src/Compilers/Z/Inline.v +++ b/src/Compilers/Z/Inline.v @@ -3,5 +3,8 @@ Require Import Crypto.Compilers.Inline. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Util. +Definition InlineConstAndOpp {t} (e : Expr base_type op t) : Expr base_type op t + := @InlineConst base_type op (is_const_or_opp) t e. + Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t := @InlineConst base_type op (is_const) t e. |