yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

[helm.git] / helm / software / matita / dama / excess.ma

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index c7d31c2295da159bbbb720713ce260dacbf27d65..55f531a9b53f7ff5016d16b42323cfa914555bb8 100644 (file)
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -51,7 +51,7 @@ record apartness : Type ≝ {
   ap_cotransitive: cotransitive ? ap_apart
 }.
 
-notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}.
+notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}.
 interpretation "apartness" 'apart x y = 
   (cic:/matita/excess/ap_apart.con _ x y).
 
@@ -73,7 +73,7 @@ coercion cic:/matita/excess/apart_of_excess.con.
 
 definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
 
-notation "a break ≈ b" non associative with precedence 50 for @{ 'napart $a $b}.    
+notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.    
 interpretation "alikeness" 'napart a b =
   (cic:/matita/excess/eq.con _ a b).