Changeset 2908 for src/Pugs/Class.hs

Timestamp:

05/10/05 00:06:01 (4 years ago)

Author:

mugwump

svk:copy_cache_prev:

4437

Message:

Change ∃ to ∀ when it was actually intended to be "For all"

Files:

• src/Pugs/Class.hs (modified) (5 diffs)

src/Pugs/Class.hs

@@ -50 +50 @@
     multiple inheritance model.
 
-    ∃ MetaClass A, B : A.clsSuper = B ↔ A ∈ B.clsSupClasses
+    ∀ MetaClass A, B : A.clsSuper = B ↔ A ∈ B.clsSupClasses
 
 -}
@@ -95 +95 @@
 {-
 
-    ∃ MetaClass A, MetaAssoc C : A.clsCats ∋ C ↔ C.catClass = A
-
-    ∃ MetaAssoc C₁, C₂ : C₁.catPair = C₂ ↔ C₂.catPair = C₁
+    ∀ MetaClass A, MetaAssoc C : A.clsCats ∋ C ↔ C.catClass = A
+
+    ∀ MetaAssoc C₁, C₂ : C₁.catPair = C₂ ↔ C₂.catPair = C₁
 
     -- can't be composite both ways
 
-    ∃ MetaAssoc C₁, C₂ : C₁.catPair = C₂ ∧ C₁.catIsComposite
+    ∀ MetaAssoc C₁, C₂ : C₁.catPair = C₂ ∧ C₁.catIsComposite
          → ¬(C₂.catIsComposite)
 
     -- this seems the simplest way to specify complementary categories
 
-    ∃ MetaAssoc C₁, C₂, MetaClass M₁, M₂
+    ∀ MetaAssoc C₁, C₂, MetaClass M₁, M₂
        : C₁.catPair = C₂ ∧ C₁.catClass = M₁ ∧ C₂.catClass = M₂
        → (   ∃ M₁.clsCats{C₂.catCompanion}
@@ -126 +126 @@
 {-
   simple range sanity stuff... enforce ordering
-    ∃ Range R : R[0] = One → R[1] ∈ ( One | Many )
-    ∃ Range R : R[1] = One → R[0] ∈ ( Zero | One )
-    ∃ Range R : R[0] = Many → R[1] = Many
-    ∃ Range R : R[1] = Zero → R[1] = Zero
+    ∀ Range R : R[0] = One → R[1] ∈ ( One | Many )
+    ∀ Range R : R[1] = One → R[0] ∈ ( Zero | One )
+    ∀ Range R : R[0] = Many → R[1] = Many
+    ∀ Range R : R[1] = Zero → R[1] = Zero
 
  -}
@@ -147 +147 @@
     child member of N₁ within the tree it exists in)
 
-    ∃ initTree Node N₁, N₂, MetaClass M₁, M₂ 
+    ∀ initTree Node N₁, N₂, MetaClass M₁, M₂ 
       : N₁ ∋ N₂ ∧ N₁ = M₁.clsName ∧ N₂ = M₂.clsName
       → M₁.subClasses ∋ M₂ 
@@ -253 +253 @@
   -- starting to look like the beginning again?  :)
 
-  ∃ Class C₁, C₂ : C₁.superClasses ∋ C₂
+  ∀ Class C₁, C₂ : C₁.superClasses ∋ C₂
                  ↔ C₂.subClasses ∋ C₁ ∧ C₂ ∉ C₁.subClasses
 
   -- hmm, anyone know how to induct the above to disallow circular inheritance?
 
-  -- perhaps stating axioms here isn't the right place, anyway.
   -- & (reading TAPL)