Compact definition lists

[hoheinzollern]

Currently, markdown-it-deflist does not allow compact definition lists, but these are part of the pandoc markdown spec

It would be desirable to have this feature in the library.

Theres a corresponding bug in the markdown-it-deflist plugin: markdown-it/markdown-it-deflist#12

The branch https://github.com/hoheinzollern/rocqnavi/tree/deflist introduces the extension for definition lists.

[hoheinzollern]

Example documentation for probability.v using definition lists:

(**md**************************************************************************)
(* # Probability                                                              *)
(*                                                                            *)
(* This file provides basic notions of probability theory. See `measure.v`    *)
(* for the type `probability T R` (a measure that sums to 1).                 *)
(*                                                                            *)
(*                                                                            *)
(* `{RV P >-> T'}`                                                            *)
(*     ~ random variable: a measurable function to the `measurableType T'`    *)
(*       from the measured space characterized by the probability `P`         *)
(*                                                                            *)
(* `distribution P X`                                                         *)
(*     ~ measure image of the probability measure `P` by the random variable  *)
(*       `X : {RV P -> T'}`                                                   *)
(*     ~ `P` has type `probability T R` with `T` of type `measurableType`.    *)
(*     ~ Declared as an instance of probability measure.                      *)
(*                                                                            *)
(* `'E_P[X]`                                                                  *)
(*     ~ expectation of the real measurable function X                        *)
(*                                                                            *)
(* `covariance X Y`                                                           *)
(*     ~ covariance between real random variable X and Y                      *)
(*                                                                            *)
(* `'V_P[X]`                                                                  *)
(*     ~ variance of the real random variable `X`                             *)
(*                                                                            *)
(* `'M_ X`                                                                    *)
(*     ~ moment generating function of the random variable `X`                *)
(*                                                                            *)
(* `{dmfun T >-> R}`                                                          *)
(*     ~ type of discrete real-valued measurable functions                    *)
(*                                                                            *)
(* `{dRV P >-> R}`                                                            *)
(*     ~ real-valued discrete random variable                                 *)
(*                                                                            *)
(* `dRV_dom X`                                                                *)
(*     ~ domain of the discrete random variable `X`                           *)
(*                                                                            *)
(* `dRV_enum X`                                                               *)
(*     ~ bijection between the domain and the range of `X`                    *)
(*                                                                            *)
(* `pmf X r`                                                                  *)
(*     ~ `fine (P (X @^-1` [set r]))`                                         *)
(*                                                                            *)
(* `cdf X r`                                                                  *)
(*     ~ cumulative distribution function of `X`                              *)
(*     ~ `:= distribution P X `]-oo, r]`                                      *)
(*                                                                            *)
(* `enum_prob X k`                                                            *)
(*     ~ probability of the kth value in the range of `X`                     *)
(*                                                                            *)
(* `bernoulli_pmf p`                                                          *)
(*     ~ Bernoulli pmf with parameter `p : R`                                 *)
(*                                                                            *)
(* `bernoulli p`                                                              *)
(*     ~ Bernoulli probability measure when `0 <= p <= 1` and `\d_false`      *)
(*       otherwise                                                            *)
(*                                                                            *)
(* `binomial_pmf n p`                                                         *)
(*     ~ binomial pmf with parameters `n : nat` and `p : R`                   *)
(*                                                                            *)
(* `binomial_prob n p`                                                        *)
(*     ~ binomial probability measure when `0 <= p <= 1` and `\d_0%N`         *)
(*       otherwise                                                            *)
(*                                                                            *)
(* `bin_prob n k p`                                                           *)
(*     ~ $\binom{n}{k}p^k (1-p)^{(n-k)}$                                      *)
(*     ~ Computes a binomial distribution term for $k$ successes in $n$       *)
(*       trials with success rate $p$                                         *)
(*                                                                            *)
(* `uniform_pdf a b`                                                          *)
(*     ~ uniform pdf over the interval $[a,b]$                                *)
(*                                                                            *)
(* `uniform_prob a b ab`                                                      *)
(*     ~ uniform probability over the interval $[a,b]$ where `ab0` a proof    *)
(*       that `0 < b - a`                                                     *)
(*                                                                            *)
(* `normal_peak s`                                                            *)
(*     ~ `(sqrtr (s ^+ 2 * pi *+ 2))^-1`                                      *)
(*                                                                            *)
(* `normal_fun m s x`                                                         *)
(*     ~ `expR (- (x - m) ^+ 2 / (s ^+ 2 *+ 2))`                              *)
(*                                                                            *)
(* `normal_pdf m s`                                                           *)
(*     ~ pdf of the normal distribution with mean `m` and standard deviation  *)
(*       `s`                                                                  *)
(*     ~ Using normal_peak and normal_pdf.                                    *)
(*                                                                            *)
(* `normal_prob m s`                                                          *)
(*     ~ normal probability measure                                           *)
(*                                                                            *)
(******************************************************************************)

The idea would be to remove the empty lines.

[hoheinzollern]

Also a start of a header for measure.v:

(**md**************************************************************************)
(* # Measure Theory                                                           *)
(*                                                                            *)
(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.   *)
(*                                                                            *)
(* This files provides a formalization of the basics of measure theory. This  *)
(* includes the formalization of mathematical structures and of measures, as  *)
(* well as standard theorems such as the Measure Extension theorem that       *)
(* builds a measure given a function defined over a semiring of sets, the     *)
(* intermediate outer measure being                                           *)
(* $\inf_F\{ \sum_{k=0}^\infty \mu(F_k)  | X \subseteq \bigcup_k F_k\}.$      *)
(*                                                                            *)
(* References:                                                                *)
(* - R. Affeldt, C. Cohen. Measure construction by extension in dependent     *)
(*   type theory with application to integration. JAR 2023                    *)
(* - Daniel Li. Intégration et applications. 2016                             *)
(* - Achim Klenke. Probability Theory. 2014                                   *)
(*                                                                            *)
(* ## Mathematical structures                                                 *)
(* `semiRingOfSetsType d`                                                     *)
(*   ~ the type of semirings of sets                                          *)
(*   ~ The carrier is a set of sets A_i such that "measurable A_i" holds.     *)
(*   ~ `measurable A` is printed as `d.-measurable A` where d is a "display   *)
(*     parameter" whose purpose is to distinguish different `measurable`      *)
(*     predicates in the same context.                                        *)
(*   ~ The HB class is `SemiRingOfSets`.                                      *)
(*                                                                            *)
(* `ringOfSetsType d`                                                         *)
(*   ~ the type of rings of sets                                              *)
(*   ~ The HB class is `RingOfSets`.                                          *)
(*                                                                            *)
(* `sigmaRingType d`                                                          *)
(*   ~ the type of sigma-rings (of sets)                                      *)
(*   ~ The HB class is `SigmaRing`.                                           *)
(*                                                                            *)
(* `algebraOfSetsType d`                                                      *)
(*   ~ the type of algebras of sets                                           *)
(*   ~ The HB class is `AlgebraOfsets`.                                       *)
(*                                                                            *)
(* `measurableType`                                                           *)
(*   ~ the type of sigma-algebras                                             *)
(*   ~ The HB class is `Measurable`.                                          *)
(*                                                                            *)

both would look much better if there wasn't an empty line between definitions.