From 2b955907c0743164bae977c3e56480d843e1bc0b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 14:20:47 +0200
Subject: [PATCH] Added todo in regards to ltyped_val explanation

---
 theories/logrel/term_typing_judgment.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index d28e25b..73de0d0 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -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 := {}.
-- 
GitLab