Changeset 2951 for extracted/fixpoints.mli
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/fixpoints.mli
r2773 r2951 140 140 141 141 type fixpoint = 142 equations >valuation142 valuation 143 143 (* singleton inductive, whose constructor was mk_fixpoint *) 144 144 145 145 val fixpoint_rect_Type4 : 146 property_lattice > ((equations > valuation)> __ > 'a1) > fixpoint >146 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 147 147 'a1 148 148 149 149 val fixpoint_rect_Type5 : 150 property_lattice > ((equations > valuation)> __ > 'a1) > fixpoint >150 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 151 151 'a1 152 152 153 153 val fixpoint_rect_Type3 : 154 property_lattice > ((equations > valuation)> __ > 'a1) > fixpoint >154 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 155 155 'a1 156 156 157 157 val fixpoint_rect_Type2 : 158 property_lattice > ((equations > valuation)> __ > 'a1) > fixpoint >158 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 159 159 'a1 160 160 161 161 val fixpoint_rect_Type1 : 162 property_lattice > ((equations > valuation)> __ > 'a1) > fixpoint >162 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 163 163 'a1 164 164 165 165 val fixpoint_rect_Type0 : 166 property_lattice > ((equations > valuation)> __ > 'a1) > fixpoint >167 'a1 168 169 val fix_lfp : property_lattice > fixpoint > equations> valuation166 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 167 'a1 168 169 val fix_lfp : property_lattice > equations > fixpoint > valuation 170 170 171 171 val fixpoint_inv_rect_Type4 : 172 property_lattice > fixpoint > ((equations > valuation) > __ > __ >173 'a1)> 'a1172 property_lattice > equations > fixpoint > (valuation > __ > __ > 'a1) 173 > 'a1 174 174 175 175 val fixpoint_inv_rect_Type3 : 176 property_lattice > fixpoint > ((equations > valuation) > __ > __ >177 'a1)> 'a1176 property_lattice > equations > fixpoint > (valuation > __ > __ > 'a1) 177 > 'a1 178 178 179 179 val fixpoint_inv_rect_Type2 : 180 property_lattice > fixpoint > ((equations > valuation) > __ > __ >181 'a1)> 'a1180 property_lattice > equations > fixpoint > (valuation > __ > __ > 'a1) 181 > 'a1 182 182 183 183 val fixpoint_inv_rect_Type1 : 184 property_lattice > fixpoint > ((equations > valuation) > __ > __ >185 'a1)> 'a1184 property_lattice > equations > fixpoint > (valuation > __ > __ > 'a1) 185 > 'a1 186 186 187 187 val fixpoint_inv_rect_Type0 : 188 property_lattice > fixpoint > ((equations > valuation) > __ > __ > 189 'a1) > 'a1 190 191 val fixpoint_discr : property_lattice > fixpoint > fixpoint > __ 192 193 val fixpoint_jmdiscr : property_lattice > fixpoint > fixpoint > __ 188 property_lattice > equations > fixpoint > (valuation > __ > __ > 'a1) 189 > 'a1 190 191 val fixpoint_discr : 192 property_lattice > equations > fixpoint > fixpoint > __ 193 194 val fixpoint_jmdiscr : 195 property_lattice > equations > fixpoint > fixpoint > __ 196 197 val dpi1__o__fix_lfp__o__inject : 198 property_lattice > equations > (fixpoint, 'a1) Types.dPair > valuation 199 Types.sig0 200 201 val eject__o__fix_lfp__o__inject : 202 property_lattice > equations > fixpoint Types.sig0 > valuation 203 Types.sig0 204 205 val fix_lfp__o__inject : 206 property_lattice > equations > fixpoint > valuation Types.sig0 194 207 195 208 val dpi1__o__fix_lfp : 196 property_lattice > (fixpoint, 'a1) Types.dPair > equations> valuation209 property_lattice > equations > (fixpoint, 'a1) Types.dPair > valuation 197 210 198 211 val eject__o__fix_lfp : 199 property_lattice > fixpoint Types.sig0 > equations > valuation 200 201 type fixpoint_computer = property_lattice > fixpoint 202 212 property_lattice > equations > fixpoint Types.sig0 > valuation 213 214 type fixpoint_computer = property_lattice > equations > fixpoint 215 216 val dpi1__o__apply_fixpoint : 217 property_lattice > equations > (fixpoint, 'a1) Types.dPair > 218 Graphs.label > __ 219 220 val eject__o__apply_fixpoint : 221 property_lattice > equations > fixpoint Types.sig0 > Graphs.label > __ 222
Note: See TracChangeset
for help on using the changeset viewer.