From ec8a7d86e08d5e67747ddb30b4badaaec5306447 Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Tue, 16 Jul 2024 10:54:58 +0200
Subject: [PATCH] Explain if_pos/if_neg in addition to dif_pos/dif_neg

---
 MIL/C04_Sets_and_Functions/S02_Functions.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/MIL/C04_Sets_and_Functions/S02_Functions.lean b/MIL/C04_Sets_and_Functions/S02_Functions.lean
index c6f2556e..dddadc64 100644
--- a/MIL/C04_Sets_and_Functions/S02_Functions.lean
+++ b/MIL/C04_Sets_and_Functions/S02_Functions.lean
@@ -565,6 +565,8 @@ since in the positive case, the value returned,
 The identity ``dif_pos h`` rewrites ``if h : e then a else b``
 to ``a`` given ``h : e``,
 and, similarly, ``dif_neg h`` rewrites it to ``b`` given ``h : ¬ e``.
+There are also versions ``if_pos`` and ``if_neg`` that works for non-dependent
+if constructions and will be used in the next section.
 The theorem ``inverse_spec`` says that ``inverse f``
 meets the first part of this specification.