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

Added todo for ltyped_val_lam deriving

parent 55b265fa
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
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