aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Inline.v
blob: df46c0ecf65c5a84e194402fc395a5e1f5e12991 (plain)
1
2
3
4
5
6
7
8
9
10
Require Import Crypto.Compilers.Syntax.
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.