diff options
Diffstat (limited to 'src/Compilers/ZExtended/MapBaseType.v')
| -rw-r--r-- | src/Compilers/ZExtended/MapBaseType.v | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/src/Compilers/ZExtended/MapBaseType.v b/src/Compilers/ZExtended/MapBaseType.v deleted file mode 100644 index 66b18f6f5..000000000 --- a/src/Compilers/ZExtended/MapBaseType.v +++ /dev/null @@ -1,22 +0,0 @@ -Require Import Coq.ZArith.BinIntDef. -Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.ZExtended.Syntax. -Require Import Crypto.Compilers.ZExtended.Syntax.Util. -Require Import Crypto.Compilers.MapBaseType. - -Definition MapBaseType' {t} (e : Expr t) - : Z.Syntax.Expr (Arrow (lift_flat_type unextend_base_type (domain t)) - (lift_flat_type unextend_base_type (codomain t))) - := @MapBaseType' _ _ _ _ unextend_base_type (fun _ s d opc _ => unextend_op opc) - (fun _ t => Op (make_const t (ZToInterp 0)) TT) - t e. - -Definition MapBaseType {t} (e : Expr t) - : option (Z.Syntax.Expr (Arrow (lift_flat_type unextend_base_type (domain t)) - (lift_flat_type unextend_base_type (codomain t)))) - := @MapBaseType _ _ _ _ unextend_base_type (fun _ s d opc _ => unextend_op opc) - (fun _ t => Op (make_const t (ZToInterp 0)) TT) - t e. |