docgen parameters in inductives

Stream: general

[Mario Carneiro]

The printout here looks wrong: https://leanprover-community.github.io/mathlib_docs/computability/turing_machine.html#turing.TM2.stmt

inductive turing.​TM2.​stmt {K : Type u_1} [decidable_eq K] :
  (K → Type u_2) → Type u_3 → Type u_4 → Type (max u_1 u_2 u_3 u_4)
| push : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) (k : K), (σ → Γ k) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
| peek : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) (k : K), (σ → option (Γ k) → σ) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
| pop : Π {K : Type u_1} [_inst_1 : decidable_eq K] (Γ : K → Type u_2) (Λ : Type u_3) (σ : Type u_4) (k : K), (σ → option (Γ k) → σ) → turing.TM2.stmt Γ Λ σ → turing.TM2.stmt Γ Λ σ
...

1. The arguments K _inst_1 Γ Λ σ should be elided from the constructors
2. The colon should be to the right of these arguments in the type itself

[Mario Carneiro]

I thought that (1) was an issue related to the use of parameters in this file, but even list has the same issue

[Eric Wieser]

Opened leanprover-community/doc-gen#159 to track this