haveI, exact statements in theorems are not shown

[eric-wieser]

The statement of module_ext is

lemma module_ext {R : Type*} [ring R] {M : Type*} [add_comm_group M] (P Q : module R M)
  (w : ∀ (r : R) (m : M), by { haveI := P, exact r • m } = by { haveI := Q, exact r • m }) :
  P = Q :=

but the docs show it as

theorem module_ext {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] (P Q : module R M) :
(∀ (r : R) (m : M), r • m = r • m) → P = Q

This is obviously unhelpful, as r • m = r • m is just rfl, unlike the original theorem which is not.

[digama0]

I don't see any reasonable way to fix this. Lean has no idea we're doing funny business with terms, and docgen can't reflect on lean syntax. The best you can hope for in the near term is to document lemmas with this pattern so that the comments show what's really going on.

[robertylewis]

I agree with Mario. Note that #check module_ext prints the same. The docs aren't generated from the input files (nor should they be), they're generated from the compiled library by printing each declaration. Changing this means implementing a new pretty printer and it's far from clear how that should behave.

[eric-wieser]

Right - so this is presumably an issue in the pretty-printer and not the docs at all. Should this issue be moved to the lean repo?

[robertylewis]

I don't think it's an issue. The pretty printer is doing what it's supposed to. Both of those terms are r • m (with different implicit arguments), what do you expect the pretty printer to do?

[eric-wieser]

Perhaps show implicit arguments if they cannot be inferred unambiguously

[gebner]

I don't think there's anything we can realistically do to fix this in Lean 3. IIRC this will be fixed in Lean 4.