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

fix linebreak behavior for binary update modalities

parent cde85898
No related branches found
No related tags found
No related merge requests found
......@@ -75,3 +75,25 @@
--------------------------------------∗
True
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
E : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP ={E}=∗
QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP ={E1,E2}=∗
QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
......@@ -517,6 +517,17 @@ Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P :
Proof.
iIntros "?". Show.
Abort.
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ QQQQQQQQQQQQQQQQQQ QQQQQQQQQQQQQQQQQQ.
Proof.
iStartProof. Show.
Abort.
Lemma long_fupd_maskchanging E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ QQQQQQQQQQQQQQQQQQ QQQQQQQQQQQQQQQQQQ.
Proof.
iStartProof. Show.
Abort.
End linebreaks.
End printing_tests.
......@@ -50,34 +50,35 @@ Reserved Notation "'<subj>' P" (at level 20, right associativity).
(** Update modalities *)
Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==> Q").
Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P ==∗ Q").
Reserved Notation "P ==∗ Q"
(at level 99, Q at level 200, format "'[hv ' P ==∗ '/' Q ']'").
Reserved Notation "|={ E1 , E2 }=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q").
Reserved Notation "P ={ E1 , E2 }=∗ Q"
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q").
format "'[hv ' P ={ E1 , E2 }=∗ '/' Q ']'").
Reserved Notation "|={ E }=> Q"
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q").
Reserved Notation "P ={ E }=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q").
format "'[hv ' P ={ E }=∗ '/' Q ']'").
Reserved Notation "|={ E1 , E2 }▷=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }▷=> Q").
Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }▷=∗ Q").
format "'[hv ' P ={ E1 , E2 }▷=∗ '/' Q ']'").
Reserved Notation "|={ E }▷=> Q"
(at level 99, E at level 50, Q at level 200,
format "|={ E }▷=> Q").
Reserved Notation "P ={ E }▷=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "P ={ E }▷=∗ Q").
format "'[hv ' P ={ E }▷=∗ '/' Q ']'").
(** Big Ops *)
Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment