Changeset 2883 for src/ERTLptr/liveness.ma
- Timestamp:
- Mar 15, 2013, 6:33:18 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTLptr/liveness.ma
r2700 r2883 26 26 〈set_empty …, set_singleton … r〉. 27 27 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〉.28 definition pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B. 29 A × B → A × B → A × B≝ 30 λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉. 31 32 definition rl_join: register_lattice → register_lattice → register_lattice ≝ 33 pairwise ?? (set_union …) (set_union …). 34 34 35 35 definition 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〉. 36 pairwise ?? (set_diff …) (set_diff …). 41 37 42 38 definition defined ≝
Note: See TracChangeset
for help on using the changeset viewer.