Changeset 1077 for src/common


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

ack, dependent types are scary

Location:
src/common
Files:
2 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 ?.
  • src/common/Identifiers.ma

    r1072 r1077  
    139139  ].
    140140
    141 axiom fold:
     141axiom foldi:
    142142  ∀A, B: Type[0].
    143143  ∀tag: String.
Note: See TracChangeset for help on using the changeset viewer.