fsdoc: no-summary-found
fsdoc: no-comment-found
**** Some predicates ********* Mem definition ********* Lemmas about mem and predicates ********** map_invariant related lemmas ********* downward_closed related lemmas ********** tip_top related lemmas ********* rid_ctr_pred related lemmas ********* Operations on mem ********* The following two lemmas are only used in FStar.Pointer.Base, and invoked explicitly ********* API for generating modifies clauses in the old style, should use new modifies clauses now ********* Lemmas about equality of mem ****** Untyped views of references