> If you've spent a significant amount of time with such proof assistants, you'd see that the proof search is rather pitiful. Afaik, Idris' proof search was ha

> If you've spent a significant amount of time with such proof assistants, you'd see that the proof search is rather pitiful. Afaik, Idris' proof search was hacked together in an afternoon just to see if it would work. And it did, surprisingly well considering. Don't know how much it has been worked on since then though. But yes, still leaves a bit to be desired compared to other systems.