Skip to content
Snippets Groups Projects

rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

Merged Ralf Jung requested to merge ralf/intuitionistically into gen_proofmode
Files
20
@@ -68,4 +68,4 @@ Proof.
iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
iExists (R Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
Qed.
End fupd.
\ No newline at end of file
End fupd.
Loading