TBH I actually think the documentation for Idris is quite good, but your overall point is correct: it's definitely somewhere between "academic toy" and "serious language". It's not really usable for anything real world at the moment, and - like I comment every time it pops up here - just as it was building up momentum the author scrapped the whole thing and started over (Idris 2), and even though I've been making that comment for years it still hasn't recovered. The book everyone recommends to read on it is based around a dead version of the language; the tooling it has you use (which is a huge part of working with a dependently-typed language) depends on Atom, which is now dead, and Idris 2 still doesn't have comparable IDE support.
I find it really frustrating because I like the language a lot, and I want to be using dependent types in my real life ASAP. Right now I'd be looking more towards Lean, though, which seems to be more modern and developing rapidly.
The Atom implementation has been replicated in VSCode and works alright. It was good enough for me to learn how Idris worked and go through the book's exercises.
I find it really frustrating because I like the language a lot, and I want to be using dependent types in my real life ASAP. Right now I'd be looking more towards Lean, though, which seems to be more modern and developing rapidly.