standardization: equivalence between paths and left residuals started

[helm.git] / matita / matita / contribs / lambda / background / notation.ma

diff --git a/matita/matita/contribs/lambda/background/notation.ma b/matita/matita/contribs/lambda/background/notation.ma
index c698a5b12a658d6548592520c4077aff93bd7980..62b8b2dcadd3a974d1b4749e633e03a385bf3236 100644 (file)
--- a/matita/matita/contribs/lambda/background/notation.ma
+++ b/matita/matita/contribs/lambda/background/notation.ma
@@ -14,6 +14,16 @@
 
 (* GENERIC NOTATION *********************************************************)
 
+(* Note: this should go to core_notation *)
+notation "⊥"
+  non associative with precedence 90
+  for @{'false}.
+
+(* Note: this should go to core_notation *)
+notation "⊤"
+  non associative with precedence 90
+  for @{'true}.
+
 (* Note: this should go to core_notation *)
 notation "hvbox(a break ≺ b)"
    non associative with precedence 45