Ralf Jung (May 13 2022 at 07:51): Ralf Jung (May 13 2022 at 07:51):We have a comment like this in our code:
(** The general approach we use for all these complex notations: an outer '[hv'
to switch bwteen "horizontal mode" where it all fits on one line, and "vertical
mode" where each '/' becomes a line break. Then, as appropriate, nested boxes
('['...']') for things like preconditions and postconditions such that they are
maximally horizontal and suitably indented inside the parentheses that surround
them. *)
This makes coqdoc print a warning, since it tries to interpret the [ in '[hv as the beginning of inline code. Is there a way to escape the bracket so coqdoc doesnt get confused and we dont have warnings in our build?
Ana de Almeida Borges (May 13 2022 at 09:20):IIRC you can place square brackets inside other square brackets at will. So ['[hv'] should work, although it will typeset it as code.
Ana de Almeida Borges (Oct 06 2022 at 16:48):@Ralf Jung, you can also pass the --plain-comments to coqdoc
Ralf Jung (Oct 08 2022 at 09:03):that would affect all comments though, not just this one
Li-yao (Oct 08 2022 at 09:19):<<'[hv'>> (<</>> delimits code blocks)
Last updated: Jan 31 2023 at 13:02 UTC