Changeset 1077 for src/common

Timestamp:

Jul 19, 2011, 12:23:32 PM (9 years ago)

Author:

mulligan

Message:

ack, dependent types are scary

Location:

src/common

Files:

• Graphs.ma (modified) (1 diff)
• Identifiers.ma (modified) (1 diff)

src/common/Graphs.ma

@@ -11 +11 @@
 
 definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
+
+axiom graph_add:
+  ∀A: Type[0].
+  ∀g: graph A.
+  ∀l: label.
+  ∀s: A.
+    lookup ? ? (add ? ? g l s) l ≠ None ?.
+
+axiom graph_add_lookup:
+  ∀A: Type[0].
+  ∀g: graph A.
+  ∀l: label.
+  ∀s: A.
+  ∀to_insert: label.
+    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.

src/common/Identifiers.ma

@@ -139 +139 @@
   ].
 
-axiom fold:
+axiom foldi:
   ∀A, B: Type[0].
   ∀tag: String.