Commit cfd71586 authored by Daniël Louwrink's avatar Daniël Louwrink Committed by Jonas Kastberg

Add Löb TODO

parent 91af156d
...@@ -194,6 +194,8 @@ Section subtyping_rules. ...@@ -194,6 +194,8 @@ Section subtyping_rules.
iApply lty_le_exist; try (iAssumption || iApply lty_le_refl). iApply lty_le_exist; try (iAssumption || iApply lty_le_refl).
Qed. Qed.
(* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)
(* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *) (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
Lemma lty_copyable_rec C `{!Contractive C} : Lemma lty_copyable_rec C `{!Contractive C} :
( A, lty_copyable A - lty_copyable (C A)) - lty_copyable (lty_rec C). ( A, lty_copyable A - lty_copyable (C A)) - lty_copyable (lty_rec C).
......
Markdown is supported
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