diff options
Diffstat (limited to 'src/Reflection/Z/Syntax/Util.v')
| -rw-r--r-- | src/Reflection/Z/Syntax/Util.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v new file mode 100644 index 000000000..0feaa08d3 --- /dev/null +++ b/src/Reflection/Z/Syntax/Util.v @@ -0,0 +1,7 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Z.Syntax. + +Definition make_const t : interp_base_type t -> op Unit (Tbase t) + := match t with TZ => OpConst end. +Definition is_const s d (v : op s d) : bool + := match v with OpConst _ => true | _ => false end. |