aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/FoldTypes.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/FoldTypes.v')
-rw-r--r--src/Compilers/Z/FoldTypes.v17
1 files changed, 0 insertions, 17 deletions
diff --git a/src/Compilers/Z/FoldTypes.v b/src/Compilers/Z/FoldTypes.v
deleted file mode 100644
index 7b3059e43..000000000
--- a/src/Compilers/Z/FoldTypes.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Z.Syntax.
-Require Import Crypto.Compilers.Z.Syntax.Util.
-Require Import Crypto.Compilers.FoldTypes.
-
-Section min_or_max.
- Context (f : base_type -> base_type -> base_type)
- (init : base_type).
-
- Definition TypeFold {t} (e : Expr t) : base_type
- := TypeFold (fun t => t) f init e.
-End min_or_max.
-
-Definition MaxTypeUsed {t} (e : Expr t) : base_type
- := TypeFold base_type_max (TWord 0) e.
-Definition MinTypeUsed {t} (e : Expr t) : base_type
- := TypeFold base_type_min TZ e.