leanprover/doc-gen4

Mangled docstring for `CoeHTCT`

eric-wieser opened this issue · 2 comments

eric-wieser commented

I'm not sure what's going on here. The docs say

Coerces a value of type α to type β. Accessible by the notation ↑x↑x, or by double type ascription ((x : α) : β).

but the source says

  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/

Somehow ↑x ended up duplicated.

eric-wieser commented

The docstring for https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Eqns.html#Lean.Meta.GetUnfoldEqnFn is even worse, it says

(xs : Nat) →
  f xs =
    match xs with
    | [] => []
    | x::xs => (x+1)::f xs
→
  f xs =
    match xs with
    | [] => []
    | x::xs => (x+1)::f xs

but the source says

(xs : Nat) →
  f xs =
    match xs with
    | [] => []
    | x::xs => (x+1)::f xs
  • 👀1