Skip to content
Snippets Groups Projects
Commit c52fd7fa authored by Daniël Louwrink's avatar Daniël Louwrink Committed by Jonas Kastberg
Browse files

remove value restriction TODO

parent d809751b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping_rules.v
+ 0
− 1
View file @ c52fd7fa
...@@ -169,7 +169,6 @@ Section subtyping_rules. ...@@ -169,7 +169,6 @@ Section subtyping_rules.
iApply (wp_wand with "H"). iIntros (v') "H Hle' !>". iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
by iApply "Hle'". by iApply "Hle'".
Qed. Qed.
(* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
Lemma lty_le_exist C1 C2 : Lemma lty_le_exist C1 C2 :
▷ (∀ A, C1 A <: C2 A) -∗ ▷ (∀ A, C1 A <: C2 A) -∗
......
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