diff options
Diffstat (limited to 'src/Compilers/Z/Syntax/Util.v')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index b84a00dee..daf3d65be 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -18,6 +18,13 @@ Definition make_const t : interp_base_type t -> op Unit (Tbase t) Definition is_const s d (v : op s d) : bool := match v with OpConst _ _ => true | _ => false end. Arguments is_const [s d] v. +Definition is_opp s d (v : op s d) : bool + := match v with Opp _ _ => true | _ => false end. +Arguments is_opp [s d] v. +Definition is_const_or_opp s d (v : op s d) : bool + := (is_const v || is_opp v)%bool. +Arguments is_const_or_opp [s d] v. + Definition cast_back_flat_const {var t f V} (v : interp_flat_type interp_base_type (@SmartFlatTypeMap base_type var f t V)) |