Laterable cleanup
!636 (merged) made make_laterable
more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
-
Define Laterable
in terms ofmake_laterable
(seelaterable_alt
). -
Rename make_laterable
to follow our modality naming scheme...laterably
? -
Resolve TC backtracking issue around persistent_laterable
-
iMod
formake_laterable
elimination?