[dunham]

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.