summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kuncar |

Thu, 13 Feb 2014 15:51:54 +0100 | |

changeset 55457 | e373c9f60db1 |

parent 55456 | a422f93eae0d |

child 55458 | d3b72d260d4a |

more precise descripiton

--- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Feb 13 14:32:05 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Feb 13 15:51:54 2014 +0100 @@ -460,11 +460,13 @@ in (* - ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t - and T is a transfer relation between t and f. + ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer + relation for t and T is a transfer relation between t and f, which consists only from + parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes + co-variance or contra-variance. The function merges par_R OO T using definitions of parametrized correspondence relations - (e.g., rel_T R OO cr_T == pcr_T R). + (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T). *) fun merge_transfer_relations ctxt ctm =