Ayertienna
commented
11 years ago We've settled for function; we also have a more general relation (unbox M ~ unbox_fetch w N when M ~ N, for any w) for which also dynamics are done
Closed Ayertienna closed 11 years ago
Ayertienna
commented
11 years ago We've settled for function; we also have a more general relation (unbox M ~ unbox_fetch w N when M ~ N, for any w) for which also dynamics are done
Whichever version we will end up using (relation vs function) we'll need some dynamics preservation: e.g.: forall M N w, L_to_Hyb_term w M N -> forall M', step_L (M, w) (M', w) -> value_Hyb N \/ exists N', step_Hyb (N, w) (N', w) /\ L_to_Hyb_term w M' N'.