fact: Fixpoint addCacheToMethod' (Dom : list Type) (Cod : option Type) (oldMethod : methodType' rep Dom Cod) : methodType' cachedRep Dom Cod := match Dom return methodType' rep Dom Cod -> methodType' cachedRep Dom Cod with | nil => match Cod return methodType' rep nil Cod -> methodType' cachedRep nil Cod with | Some C => fun oldMethod => or <- oldMethod; cv <- {cv | cacheSpec (fst or) cv}; ret ({| origRep := (fst or); cachedVal := cv |}, snd or) | None => fun oldMethod => or <- oldMethod; cv <- {cv | cacheSpec or cv}; ret {| origRep := or; cachedVal := cv |} end | cons D Dom' => fun oldMethod (d : D) => addCacheToMethod' Dom' Cod (oldMethod d) end oldMethod.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv