blob: 776f000f5df37a468d81ded224c9f99b7828c741 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Z.Syntax.Util.
Require Import Crypto.Reflection.FoldTypes.
Section min_or_max.
Context (f : base_type -> base_type -> base_type)
(init : base_type).
Definition TypeFold {t} (e : Expr base_type op t) : base_type
:= TypeFold (fun t => t) f init e.
End min_or_max.
Definition MaxTypeUsed {t} (e : Expr base_type op t) : base_type
:= TypeFold base_type_max (TWord 0) e.
Definition MinTypeUsed {t} (e : Expr base_type op t) : base_type
:= TypeFold base_type_min TZ e.
|
