Commit 34f64c8d authored by Ralf Jung's avatar Ralf Jung

remove big_opL from prettification list

List literals reduce with a spurious `emp` at the end, which is not pretty.
parent aa6ecfbb
Pipeline #10498 passed with stage
in 30 minutes and 36 seconds
...@@ -100,6 +100,19 @@ Tactic failure: iFrame: cannot frame Q. ...@@ -100,6 +100,19 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗ --------------------------------------∗
□ P □ P
1 subgoal
PROP : sbi
x : nat
l : list nat
P : PROP
============================
"HP" : P
_ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
_ : [∗ list] y ∈ (x :: l), <affine> ⌜y = y⌝
--------------------------------------∗
P
1 subgoal 1 subgoal
PROP : sbi PROP : sbi
...@@ -113,6 +126,19 @@ Tactic failure: iFrame: cannot frame Q. ...@@ -113,6 +126,19 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗ --------------------------------------∗
P P
1 subgoal
PROP : sbi
x1, x2 : nat
l1, l2 : list nat
P : PROP
============================
"HP" : P
_ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
_ : [∗ list] y1;y2 ∈ (x1 :: l1);((x2 :: l2) ++ l2), <affine> ⌜y1 = y2⌝
--------------------------------------∗
P ∨ ([∗ list] _;_ ∈ (x1 :: l1);(x2 :: l2), True)
1 subgoal 1 subgoal
PROP : sbi PROP : sbi
......
...@@ -490,14 +490,14 @@ Lemma test_big_sepL_simpl x (l : list nat) P : ...@@ -490,14 +490,14 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
([ list] ky l, <affine> y = y ) - ([ list] ky l, <affine> y = y ) -
([ list] y x :: l, <affine> y = y ) - ([ list] y x :: l, <affine> y = y ) -
P. P.
Proof. iIntros "HP ??". Show. done. Qed. Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P : Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
P - P -
([ list] ky1;y2 []; l2, <affine> y1 = y2 ) - ([ list] ky1;y2 []; l2, <affine> y1 = y2 ) -
([ list] y1;y2 x1 :: l1; (x2 :: l2) ++ l2, <affine> y1 = y2 ) - ([ list] y1;y2 x1 :: l1; (x2 :: l2) ++ l2, <affine> y1 = y2 ) -
P ([ list] y1;y2 x1 :: l1; x2 :: l2, True). P ([ list] y1;y2 x1 :: l1; x2 :: l2, True).
Proof. iIntros "HP ?? /=". Show. by iLeft. Qed. Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
Lemma test_big_sepL2_iDestruct (Φ : nat nat PROP) x1 x2 (l1 l2 : list nat) : Lemma test_big_sepL2_iDestruct (Φ : nat nat PROP) x1 x2 (l1 l2 : list nat) :
([ list] y1;y2 x1 :: l1; x2 :: l2, Φ y1 y2) - ([ list] y1;y2 x1 :: l1; x2 :: l2, Φ y1 y2) -
......
...@@ -22,7 +22,7 @@ Declare Reduction pm_cbn := cbn [ ...@@ -22,7 +22,7 @@ Declare Reduction pm_cbn := cbn [
tele_fold tele_bind tele_app tele_fold tele_bind tele_app
(* BI connectives *) (* BI connectives *)
bi_persistently_if bi_affinely_if bi_intuitionistically_if bi_persistently_if bi_affinely_if bi_intuitionistically_if
bi_wandM sbi_laterN big_opL bi_wandM sbi_laterN
bi_tforall bi_texist bi_tforall bi_texist
]. ].
Ltac pm_eval t := Ltac pm_eval t :=
......
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