diff options
Diffstat (limited to 'src/Util/Sigma/MapProjections.v')
| -rw-r--r-- | src/Util/Sigma/MapProjections.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/Sigma/MapProjections.v b/src/Util/Sigma/MapProjections.v new file mode 100644 index 000000000..fd5556a33 --- /dev/null +++ b/src/Util/Sigma/MapProjections.v @@ -0,0 +1,6 @@ +Require Export Crypto.Util.GlobalSettings. + +Definition projT2_map {A P Q} (f : forall a, P a -> Q a) (x : @sigT A P) : @sigT A Q + := let 'existT a p := x in existT Q a (f a p). +Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : @sig A P) : @sig A Q + := let 'exist a p := x in exist Q a (f a p). |