From afff201ac24f5f3f84e7cb44f7f2228f2e2365e9 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 14:19:05 +0200
Subject: [PATCH] Added todo for ltyped_val_lam deriving

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

diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index c70cf6d..9d953dd 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -144,6 +144,7 @@ Section term_typing_rules.
     iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
   Qed.
 
+  (* TODO: This might be derivable from rec value rule *)
   Lemma ltyped_val_lam x e A1 A2 :
     ((env_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
     ⊨ᵥ (λ: x, e) : A1 ⊸ A2.
-- 
GitLab