Stream: Coq users

Topic: Escape [ for coqdoc?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Oct 06 2022 at 16:48):

@Ralf Jung, you can also pass the --plain-comments to coqdoc

view this post on Zulip Ralf Jung (Oct 08 2022 at 09:03):

that would affect all comments though, not just this one

view this post on Zulip Li-yao (Oct 08 2022 at 09:19):

<<'[hv'>> (<</>> delimits code blocks)


Last updated: Jan 31 2023 at 13:02 UTC