Changeset 1635 for src/common/Graphs.ma


Ignore:
Timestamp:
Jan 7, 2012, 12:33:17 AM (8 years ago)
Author:
tranquil
Message:
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Graphs.ma

    r1515 r1635  
    3636    lookup ? ? (add ? ? g l s) l ≠ None ?.
    3737
     38axiom graph_add_eq:
     39  ∀A: Type[0].
     40  ∀g: graph A.
     41  ∀l: label.
     42  ∀s: A.
     43    lookup ? ? (add ? ? g l s) l = Some ? s.
     44
    3845axiom graph_add_lookup:
    3946  ∀A: Type[0].
     
    4350  ∀to_insert: label.
    4451    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
     52   
     53axiom graph_add_preserve :
     54  ∀A: Type[0].
     55  ∀g: graph A.
     56  ∀l: label.
     57  ∀s: A.
     58  ∀to_insert: label.
     59  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
    4560
    4661axiom graph_num_nodes:
Note: See TracChangeset for help on using the changeset viewer.