Stream: Coq users

Topic: coqdoc `<<<`


view this post on Zulip Reynald Affeldt (Jun 09 2020 at 13:52):

Is this a bug or a misuse of coqdoc ?
"<<<" inside a comment is not rendered and causes a change of font in the generated html page.

Example: when process by coqdoc 8.11, the following comment

(* Alternative notation displays can be defined by :                          *)
(* 1. declaring a new opaque definition of type unit. Using the idiom         *)
(*    `Lemma my_display : unit. Proof. exact: tt. Qed.`                       *)
(* 2. using this symbol to tag canonical porderType structures using          *)
(*    `Canonical my_porderType := POrderType my_display my_type my_mixin`,    *)
(* 3. declaring notations for the main operations of this library, by         *)
(*    setting the first argument of the definition to the display, e.g.       *)
(*    `Notation my_syndef_le x y := @Order.le my_display _ x y.` or           *)
(*    `Notation "x <<< y" := @Order.lt my_display _ x y (at level ...).`      *)
(*    Non overloaded notations will default to the default display.           *)
(*                                                                            *)
(* One may use displays either for convenience or to disambiguate between     *)
(* different structures defined on "copies" of a type (as explained below.)   *)
(* We provide the following "copies" of types,                                *)
(* the first one is a *documented example*                                    *)
(*            natdvd := nat                                                   *)
(*                   == a "copy" of nat which is canonically ordered using    *)
(*                      divisibility predicate dvdn.                          *)
(*                      Notation %|, %<|, gcd, lcm are used instead of        *)
(*                      <=, <, meet and join.                                 *)

generates the following html page:
image.png

view this post on Zulip Cyril Cohen (Jun 09 2020 at 14:23):

Actually << is documented here


Last updated: Feb 01 2023 at 11:04 UTC