Documentation verbose

Stream: general

[Sebastien Gouezel]

An intent of the way probability theory is written in mathlib is to have notations that is pretty close to common mathematical notations. For instance, in the Lean file the strong law of large numbers reads

  (X : ℕ → Ω → ℝ) (hint : integrable (X 0))
  (hindep : pairwise (λ i j, indep_fun (X i) (X j)))
  (hident : ∀ i, ident_distrib (X i) (X 0)) :
  ∀ᵐ ω, tendsto (λ (n : ℕ), (∑ i in range n, X i ω) / n) at_top (𝓝 (𝔼[X 0]))

Note how the measure is implicit in hint or hindep or hident, and how the expectation is written using 𝔼.

Unfortunately, in the documentation all these nice features are lost (see docs#probability_theory.strong_law_ae): the measure is written explicitly, as the unreadable measure_theory.measure_space.volume, and the expectation is replaced with an integral sign. Also, all names are fully expanded, which makes it more painful to read (albeit more explicit). Are there some ways to tweak the documentation generation to make it respect more the way the files are written?

[Patrick Massot]

I'm afraid this is one more issue where it doesn't really make sense to invest time in Lean 3. The good news is it will be much easier to solve in Lean 4.

[Eric Wieser]

I don't really see how you'd solve the integral/expectation thing unless lean4 has a new type of "print only" reducibility (unfold for everything except printing)

[Eric Wieser]

I suppose it could eagerly try and print all integrals as expectations, if that's desirable

[Alexander Bentkamp]

Lean 4 can store meta data inside expressions that can be used for pretty printing. For example, there is the notation let_fun x := v; b which is sugar for (fun x => b) v. Lean remembers whether the user wrote let_fun x := v; b or (fun x => b) v and will choose the same notation in pretty printing.

[Sebastien Gouezel]

Nice!