Commit 700caaac authored by Ralf Jung's avatar Ralf Jung

test proofmode output for long lines, and fix it

parent 4946e270
......@@ -19,6 +19,46 @@
--------------------------------------□
Q ∨ P
1 subgoal
PROP : sbi
P : PROP
============================
"HP" : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P)
∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
--------------------------------------∗
P
1 subgoal
PROP : sbi
P : PROP
============================
_ : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P)
∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
--------------------------------------∗
P
1 subgoal
PROP : sbi
P : PROP
============================
"HP" : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P |
P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
--------------------------------------∗
P
1 subgoal
PROP : sbi
P : PROP
============================
_ : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P |
P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
--------------------------------------∗
P
1 subgoal
PROP : sbi
......
......@@ -37,6 +37,39 @@ Lemma demo_3 P1 P2 P3 :
P1 P2 P3 - P1 (P2 x, (P3 x = 0) P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
(* Test line breaking of long assumptions. *)
Section linebreaks.
Lemma print_long_line P :
(P P P P P P P P P P) P P P P P P P P P
- P.
Proof.
iIntros "HP". Show.
Abort.
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.
Proof.
iIntros "?". Show.
Abort.
(* This is specifically crafted such that not having the `hv` in
the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P Q)%I
(format "'TESTNOTATION' '{{' P '|' Q '}' '}'") : bi_scope.
Lemma print_long_line P :
TESTNOTATION {{ P P P P P P P P P P P P P | P P P P P P P }}
- P.
Proof.
iIntros "HP". Show.
Abort.
Lemma print_long_line_anon P :
TESTNOTATION {{ 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.
End linebreaks.
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
......
......@@ -103,8 +103,7 @@
--------------------------------------□
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
"Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗
id (na_own t E2)
"Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ id (na_own t E2)
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
......
......@@ -10,10 +10,10 @@ Arguments Esnoc {_} _%proof_scope _%string _%I.
Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
(at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope.
left associativity, format "Γ H : '[hv' P ']' '//'", only printing) : proof_scope.
Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
(at level 1, P at level 200,
left associativity, format "Γ '_' : P '//'", only printing) : proof_scope.
left associativity, format "Γ '_' : '[hv' P ']' '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Γ Δ _) Q%I)
......
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