There is no IF_then_else in the stdlib

Villetaneuse · Dec 20, 2023 · ab0244b · ab0244b
1 parent 3e3ec9f
commit ab0244b
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
@@ -138,7 +138,6 @@ Propositional Connectives
   single: or_introl (term)
   single: or_intror (term)
   single: iff (term)
-  single: IF_then_else (term)
 
 First, we find propositional calculus connectives.
 At times, it's helpful to know exactly what these notations represent.
@@ -158,7 +157,6 @@ At times, it's helpful to know exactly what these notations represent.
   | or_introl (_:A)
   | or_intror (_:B).
   Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
-  Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 
 Quantifiers
 +++++++++++