I can imagine that parsing Coq is pretty dang difficult since the user is able to essentially define and use their own syntax in the code. Also parsing Agda see

I can imagine that parsing Coq is pretty dang difficult since the user is able to essentially define and use their own syntax in the code. Also parsing Agda seems non-trivial, though likely not as hard as C++.