Changeset 1425


Ignore:
Timestamp:
Oct 20, 2011, 11:12:38 AM (9 years ago)
Author:
mulligan
Message:

changes to the fixpoint calculation in ertl

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1282 r1425  
    264264definition equations ≝ label → rhs.
    265265
    266 axiom fix_lfp: equations → valuation.
     266record fixpoint: Type[0] ≝
     267{
     268  fix_lfp    :1> equations → valuation;
     269  fix_correct:   ∀f: equations.
     270                 ∀v: label.
     271                   lattice_equal (f v (fix_lfp f)) (fix_lfp f v)
     272}.
     273
     274axiom the_fixpoint: fixpoint.
    267275
    268276definition livebefore ≝
     
    296304  λglobals.
    297305  λint_fun.
    298     fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).
     306    the_fixpoint (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracChangeset for help on using the changeset viewer.