pub fn ghost_update_ty() -> Expr
GhostUpdate: a ghost update modality |==> P (frame-preserving update). Type: IrisProp → IrisProp