Changeset 2205 for src/LTL


Ignore:
Timestamp:
Jul 18, 2012, 12:27:01 PM (7 years ago)
Author:
campbell
Message:

Get correctness.ma type checking again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r2103 r2205  
    2626  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    2727  | S n' ⇒
    28     if mem_set … visited l then
     28    if l∈visited then
    2929     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
    3030    else
     
    4242             visit globals g required visited' generated' l2 n' in
    4343            let required'' ≝ add_set ? required' l1 in
    44              if mem_set … visited' l1 then
     44             if l1 ∈ visited' then
    4545               〈required', generated''〉
    4646             else
     
    7171       [ None ⇒ 〈None …,x〉
    7272       | Some l ⇒
    73           〈if mem_set … required' l then Some ? l else None ?,
     73          〈if l ∈ required' then Some ? l else None ?,
    7474           x〉])
    7575    reversed.
Note: See TracChangeset for help on using the changeset viewer.