Skip to content
Snippets Groups Projects
Commit 79ea27b3 authored by Ralf Jung's avatar Ralf Jung
Browse files

proofmode: normalize big_opL

parent 0157c46f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/proofmode.v
+ 1
− 1
View file @ 79ea27b3
...@@ -490,7 +490,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P : ...@@ -490,7 +490,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗ ([∗ list] k↦y ∈ 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. 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 -∗
......
theories/proofmode/reduction.v
+ 2
− 1
View file @ 79ea27b3
...@@ -22,7 +22,8 @@ Declare Reduction pm_cbn := cbn [ ...@@ -22,7 +22,8 @@ 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 bi_tforall bi_texist bi_wandM big_opL
bi_tforall bi_texist
]. ].
Ltac pm_eval t := Ltac pm_eval t :=
let u := eval pm_cbv in t in let u := eval pm_cbv in t in
......
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