fsdoc: no-summary-found
fsdoc: no-comment-found
* The modifies clause val loc_union_idem:#aloc:aloc_t -> #c:cls aloc -> s:loc c -> (Lemma (==(loc_union s s, s)))The following is useful to make Z3 cut matching loops with modifies_trans and modifies_refl
Liveness-insensitive memory locations The modifies clause proper BEGIN TODO: move to FStar.Monotonic.HyperStack END TODO * Compositionality