Stream: Coq devs & plugin devs

Topic: Struggling to understand Pp boxes


view this post on Zulip walker (Aug 06 2022 at 21:52):

I was under the impresion that hov addes n spaces before a block of code, but I was totally wrong, All I was able to understan is that it is used to create boxes, but what extactly are those boxes supposed to do? Also if they are not for creating spaces/tabs, is there an automatic way to auto indent code block when doing custom extraction plugin ?

view this post on Zulip walker (Aug 06 2022 at 21:54):

Also I see there are variants hv, v and hov but I cannot guess what each is supposed to do ? I assume h is for horizontal something and v is for vertical but I cannot understand the semantics

view this post on Zulip Emilio Jesús Gallego Arias (Aug 06 2022 at 23:47):

The semantics are indeed tricky; Coq boxes are mapped directly to OCaml's Format boxes, see the docs https://v2.ocaml.org/api/Format.html


Last updated: Feb 05 2023 at 20:03 UTC