Changeset 2949 for src/utilities
- Timestamp:
- Mar 25, 2013, 9:48:01 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/fixpoints.ma
r2700 r2949 13 13 definition equations ≝ λlatt : property_lattice.label → rhs latt. 14 14 15 record fixpoint (latt : property_lattice) : Type[0] ≝16 { fix_lfp : 1> equations latt →valuation latt15 record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝ 16 { fix_lfp :> valuation latt 17 17 ; fix_correct : 18 ∀eqs : equations latt.19 let sol ≝ fix_lfp eqs in20 18 ∀l : label. 21 l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *) 19 (* inclusion suffices for correctness *) 20 l_included latt (eqs l fix_lfp) (fix_lfp l) 22 21 }. 23 22 24 definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt. 23 definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs. 24 25 coercion apply_fixpoint: 26 ∀latt,eqs.∀f:fixpoint latt eqs. label → latt ≝ 27 λlatt,eqs,f,l. fix_lfp … f l 28 on _f: fixpoint ? ? to label → ?.
Note: See TracChangeset
for help on using the changeset viewer.