Changeset 2911 for src/Pugs/Class.hs

Timestamp:

05/10/05 02:16:17 (4 years ago)

Author:

mugwump

svk:copy_cache_prev:

4437

Message:

* explanatory essay in MetaAssoc?
* added missing clause on a Class.hs rule
* convert ∃ → ∀ in MetaClass?

Files:

• src/Pugs/Class.hs (modified) (1 diff)

src/Pugs/Class.hs

@@ -107 +107 @@
 
     ∀ MetaAssoc C₁, C₂, MetaClass M₁, M₂
-       : C₁.catPair = C₂ ∧ C₁.catClass = M₁ ∧ C₂.catClass = M₂
+       :   C₁.catPair = C₂  ∧ C₁.assocCompanion
+         ∧ C₁.catClass = M₁ ∧ C₂.catClass = M₂
        → (   ∃ M₁.clsCats{C₂.catCompanion}
            ∧ ∃ M₂.clsCats{C₁.catCompanion}