Commit 98caeb8a authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Minor clean up

parent 709a0598
......@@ -7,11 +7,6 @@ From iris.base_logic Require Import invariants.
Section Examples.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
Definition seq_example : expr :=
(let: "c" := new_chan #() in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment