Changeset 1077 for src/common/Graphs.ma


Ignore:
Timestamp:
Jul 19, 2011, 12:23:32 PM (9 years ago)
Author:
mulligan
Message:

ack, dependent types are scary

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Graphs.ma

    r746 r1077  
    1111
    1212definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
     13
     14axiom 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
     21axiom 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 ?.
Note: See TracChangeset for help on using the changeset viewer.