Skip to content
Snippets Groups Projects
Commit 49500e18 authored by Ralf Jung's avatar Ralf Jung
Browse files

change cont_postcondition to True... because we can, and because that would...

change cont_postcondition to True... because we can, and because that would allow us to show adequacy with a terminating continuation
parent 836ed650
No related branches found
No related tags found
No related merge requests found
Pipeline #
...@@ -7,7 +7,7 @@ From lrust.typing Require Import type lft_contexts type_context. ...@@ -7,7 +7,7 @@ From lrust.typing Require Import type lft_contexts type_context.
Section cont_context_def. Section cont_context_def.
Context `{typeG Σ}. Context `{typeG Σ}.
Definition cont_postcondition : iProp Σ := False%I. Definition cont_postcondition : iProp Σ := True%I.
Record cctx_elt : Type := Record cctx_elt : Type :=
CCtx_iscont { cctxe_k : val; cctxe_L : llctx; CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment