4 ms·

Which is not runnable in the first place. Interesting though, as this shows exactly the problem. It looks legit, but it's some generated fake text.

• ok123456 4y ago
  It tends to invent whole fake packages.
  • dunham 4y ago
    Yup, I got some nice documentation (minor syntax error) for a Http package in Lean that doesn't exist. I asked about Lean4 and it helpfully explained that the non-existent package had moved from Lean to Std.