theory Memory imports Utils begin class vtype = fixes to_nat :: "'a ⇒ nat option" section ‹Memory› type_synonym location = nat