Commit 96b5f919 authored by Hai Dang's avatar Hai Dang
Browse files

Remove a TODO

parent be7cb9a4
......@@ -13,7 +13,7 @@ Definition atomic_wp `{!noprolG Σ} {TA TB : tele}
(E : coPset) (* implementation masks *)
(α: TA vProp Σ) (* atomic pre-condition *)
(β: TA TB vProp Σ) (* atomic post-condition *)
(POST: TA TB vProp Σ) (* private post condition *) (* TODO: seems to be unnecessary *)
(POST: TA TB vProp Σ) (* private post condition *)
(f: TA TB val) (* Turn the return data into the return value *)
: vProp Σ :=
(Φ : val vProp Σ),
......
Supports Markdown
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