Rename push-function-into-if

Author: jamesmckinna

CHANGELOG.md

@@ -1114,6 +1114,11 @@ Deprecated names
   map-map-fusion  ↦  map-∘
   ```
 
+* In `Data.Bool.Properties` (Issue #2046):
+  ```
+  push-function-into-if ↦ if-float
+  ```
+
 * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ`
   for the 'left', resp. 'right' injection of a Fin m into a 'larger' type,
   `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the
@@ -1138,7 +1143,7 @@ Deprecated names
 
   As with Issue #1726 above: the deprecation of relation `_≺_` means that these definitions
   associated with wf-recursion are deprecated in favour of their `_<_` counterparts.
-  But it's not quite sensible to say that these definiton should be *renamed* to *anything*,
+  But it's not quite sensible to say that these definitions should be *renamed* to *anything*,
   least of all those counterparts... the type confusion would be intolerable.
 
 * In `Data.Fin.Properties`:

src/Data/Bool/Properties.agda

@@ -768,7 +768,21 @@ proof (T? false) = ofⁿ λ()
 T?-diag : ∀ b → T b → True (T? b)
 T?-diag true  _ = _
 
-push-function-into-if : ∀ (f : A → B) x {y z} →
-                        f (if x then y else z) ≡ (if x then f y else f z)
-push-function-into-if _ true  = refl
-push-function-into-if _ false = refl
+if-float : ∀ (f : A → B) b {x y} →
+           f (if b then x else y) ≡ (if b then f x else f y)
+if-float _ true  = refl
+if-float _ false = refl
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+push-function-into-if = if-float
+{-# WARNING_ON_USAGE push-function-into-if
+"Warning: push-function-into-if was deprecated in v2.0.
+Please use if-float instead."
+#-}