From bbe39a14c22dad4eea58c4d249b57c0018593b2c Mon Sep 17 00:00:00 2001
From: Calin Diacicov <diacicov.calin@gmail.com>
Date: Tue, 24 Dec 2024 00:55:53 +0200
Subject: [PATCH] Removed notation for predicate operations.

---
 code/Inductive/Predicates.v | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/code/Inductive/Predicates.v b/code/Inductive/Predicates.v
index bc8d01a..9888f77 100644
--- a/code/Inductive/Predicates.v
+++ b/code/Inductive/Predicates.v
@@ -11,16 +11,10 @@ properties.
 Section Operations.
 
   Definition predconj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∧ (q x)).
-
-  Infix "p ∧ q" := (predconj p q) (at level 25).
   
   Definition preddisj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∨ (q x)).
 
-  Infix "p ∨ q" := (preddisj p q) (at level 25).
-  
   Definition predneg {X : UU} (p : X → hProp) : X → hProp := (λ x : X, hneg (p x)).
-  
-  Notation "¬ p" := (predneg p) (at level 35).
 
   Definition preddirprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X × Y) → hProp := (λ x : X × Y, (p (pr1 x)) ∧ (q (pr2 x))). 
 
@@ -36,4 +30,6 @@ Section Operations.
 
   Definition truepred (X : UU) : X → hProp := (λ _ , htrue). 
   
+  Definition falsepred (X : UU) : X → hProp := (λ _, hfalse).
+
 End Operations.