Changeset 1077 for src/common
- Timestamp:
- Jul 19, 2011, 12:23:32 PM (8 years ago)
- Location:
- src/common
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Graphs.ma
r746 r1077 11 11 12 12 definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag. 13 14 axiom graph_add: 15 ∀A: Type[0]. 16 ∀g: graph A. 17 ∀l: label. 18 ∀s: A. 19 lookup ? ? (add ? ? g l s) l ≠ None ?. 20 21 axiom graph_add_lookup: 22 ∀A: Type[0]. 23 ∀g: graph A. 24 ∀l: label. 25 ∀s: A. 26 ∀to_insert: label. 27 lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. -
src/common/Identifiers.ma
r1072 r1077 139 139 ]. 140 140 141 axiom fold :141 axiom foldi: 142 142 ∀A, B: Type[0]. 143 143 ∀tag: String.
Note: See TracChangeset
for help on using the changeset viewer.