Ignore:
Timestamp:
Mar 15, 2013, 6:33:18 PM (7 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/liveness.ma

    r2700 r2883  
    2626    〈set_empty …, set_singleton … r〉.
    2727
    28 definition rl_join: register_lattice → register_lattice → register_lattice ≝
    29   λleft.
    30   λright.
    31   let 〈lp, lh〉 ≝ left in
    32   let 〈rp, rh〉 ≝ right in
    33     〈set_union … lp rp, set_union … lh rh〉.
     28definition pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B.
     29A × B → A × B → A × B≝
     30λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉.
     31
     32definition rl_join: register_lattice → register_lattice → register_lattice ≝
     33pairwise ?? (set_union …) (set_union …).
    3434
    3535definition rl_diff: register_lattice → register_lattice → register_lattice ≝
    36   λleft.
    37   λright.
    38   let 〈lp, lh〉 ≝ left in
    39   let 〈rp, rh〉 ≝ right in
    40     〈set_diff … lp rp, set_diff … lh rh〉.
     36pairwise ?? (set_diff …) (set_diff …).
    4137
    4238definition defined ≝
Note: See TracChangeset for help on using the changeset viewer.