diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/MapCastByDeBruijn.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijn.v | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v deleted file mode 100644 index c08ae1298..000000000 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijn.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Z.MapCastByDeBruijn. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Compilers.Z.Bounds.Interpretation. - -Section language. - Context (round_up : nat -> option nat) - {t : type base_type}. - - Definition MapCastCompile := @MapCastCompile t. - Definition MapCastDoCast - := @MapCastDoCast - (@Bounds.interp_base_type) (@Bounds.interp_op) - (@Bounds.bounds_to_base_type round_up) - (fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _) - t. - Definition MapCastDoInterp - := @MapCastDoInterp - (@Bounds.interp_base_type) (@Bounds.bounds_to_base_type round_up) - t. - Definition MapCast e input_bounds - := MapCastDoInterp input_bounds (MapCastDoCast input_bounds (MapCastCompile e)). -End language. |