Add cast_back_flat_const

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v
index 418922e53..8e9102101 100644
--- a/src/Reflection/Z/Syntax/Util.v
+++ b/src/Reflection/Z/Syntax/Util.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.TypeUtil.
 Require Import Crypto.Reflection.TypeInversion.
@@ -18,6 +19,14 @@ Definition is_cast s d (v : op s d) : bool
   := match v with Cast _ _ => true | _ => false end.
 Arguments is_cast [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))
+  : interp_flat_type interp_base_type t
+  := @SmartFlatTypeMapUnInterp
+       _ var interp_base_type interp_base_type
+       f (fun _ _ => cast_const)
+       t V v.
+
 Definition base_type_leb (v1 v2 : base_type) : bool
   := match v1, v2 with
      | _, TZ => true