bad pretty printing result #5
Comments
|
All the results are the same in coqidetop and vscoqtop, in contrast to the observation on the top post. Definition F (q w e r t y u i o p : nat) : nat := 0.
(* Notation "x = y" := (eq x y) : type_scope. *)
Goal F 111 111 111 111 111 111 111 111 111 111 = F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 =
F 111 111 111 111 111 111 111 111 111 111
*)
Abort.
Definition equiv (x y : nat) := True.
Notation "x ≡ y" := (equiv x y) (at level 70).
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111
≡ F 111 111 111 111 111 111 111 111 111 111
> For printing a notation, a formatting box is opened in such a way that if the
> notation and its arguments cannot fit on a single line, a line break is
> inserted before the symbols of the notation and the arguments on the next lines
> are aligned with the argument on the first line.
Question: Why does "x = y" notation above has break after "="?
*)
Abort.
(*
> A first, simple control that a user can have on the printing of a notation is
> the insertion of spaces at some places of the notation. This is performed by
> adding extra spaces between the symbols and parameters: each extra space (other
> than the single space needed to separate the components) is interpreted as a
> space to be inserted by the printer.
*)
Notation "x ≡ y" := (equiv x y) (at level 70).
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 ≡
F 111 111 111 111 111 111 111 111 111 111
Question: Why does this change the location of break point?
*)
Abort.
Notation "x ≡ y" := (equiv x y) (at level 70, format "x ≡ y").
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111
111 111
Question: Why no break point???
*)
Abort.
Notation "x ≡ y" := (equiv x y) (at level 70, format "'[' x ≡ '/' y ']'").
Goal F 111 111 111 111 111 111 111 111 111 111 ≡ F 111 111 111 111 111 111 111 111 111 111.
(*
F 111 111 111 111 111 111 111 111 111 111 ≡
F 111 111 111 111 111 111 111 111 111 111
*)
Abort.
Goal F 1 1 1 1 1 1 1 1 1 1 ≡ F 1 1 1 1 1 1 1 1 1 1.
(*
F 1 1 1 1 1 1 1 1 1 1 ≡F 1 1 1 1 1 1 1 1 1 1
NOTE: '/' itself doesn't occupy space.
*)
Abort. |
|
Query results don't have proper breaks. On the other hand, hover result is pre-formatted. Maybe this is the same notation issue |
|
Fixed |
|
Reported: coq/vscoq#924 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
big stuff ≡{n}≡ big stufflooks bad (when proving Contractive stuff)while
big stuff = big stuffis fine.Both look good on coqide.
This happens because the former doesn't have explicit break after
≡{n}≡.Instead, it gets
{ "Ppcmd_tag", "constr.notation", { "Ppcmd_string", " " } }.On the other hand,
=gets a break after=.Maybe
nprevents inserting break? Or is there a special treatment for builtin notations?Make an issue on iris to add
'/'?Why does it look correct in coqdie???
similar:
The text was updated successfully, but these errors were encountered: