Exponential slowdown in `iFrame` and the number of laters
From iris Require Import proofmode.tactics.
Lemma test2 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.141s *) Admitted.
Lemma test4 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 0.7s *) Admitted.
Lemma test8 {M} (P Q R : uPred M) :
(▷ P ∧ ▷ Q ∧ ▷ R) -∗ ▷ ▷ ▷ ▷ ▷ ▷ ▷ ▷ (P ∗ Q ∗ R).
Proof. Time Fail iIntros "$". (* 6.796s *) Admitted.