From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 28 Oct 2009 14:51:38 +0000 (+0000)
Subject: instances
X-Git-Tag: make_still_working~3240
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d0664747588f771e953c4d70f96e1cb5953d60e;p=helm.git

instances
---

diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index 1bb482f6e..dde57de05 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -18,10 +18,7 @@ include "nat/compare.ma".
 include "nat/minus.ma".
 include "datatypes/pairs.ma".
 
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
+alias symbol "eq" (instance 7) = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: ext_powerclass support;
diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 4703fba8c..90a644ce9 100644
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -30,17 +30,11 @@ nlemma cover_ind':
             napply infty; nauto; ##] 
 nqed.
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 1) = "covers".
 nlemma cover_ind'':
  ∀A:Ax.∀U:Ω^A.∀P:A → CProp[0].
   (∀a. a ∈ U → P a) → (∀a:A.∀j:𝐈 a. 𝐂 a j ◃ U → (∀b. b ∈ 𝐂 a j → P b) → P a) →
    ∀b. b ◃ U → P b.
-   
  #A; #U; #P; nletin V ≝ {x | P x}; napply (cover_ind' … V).
 nqed.
 
@@ -96,10 +90,8 @@ nrecord memdec (A: Type[0]) (U:Ω^A) : Type[0] ≝
 
 (*********** end from Cantor ********)
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers set".
+alias symbol "covers" (instance 9) = "covers".
+alias symbol "covers" (instance 8) = "covers".
 nlet rec cover_rect
  (A:uuAx) (U:Ω^(uuax A)) (memdec: memdec … U) (P:uuax A → Type[0])
   (refl: ∀a:uuax A. a ∈ U → P a)