Skip to content
Snippets Groups Projects
Commit 2b955907 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added todo in regards to ltyped_val explanation

parent afff201a
No related branches found
No related tags found
No related merge requests found
......@@ -42,6 +42,7 @@ Section ltyped.
Qed.
End ltyped.
(* TODO: Elaborate on why this is needed *)
Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
tc_opaque ( ltty_car A v)%I.
Instance: Params (@ltyped_val) 3 := {}.
......
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