Agda and most other dependently-typed languages (e.g. Coq) weren't really designed for "real programmers": they're research-oriented systems for real computer scientists to explore cutting edge ideas in logic and PLT.

If you're interested in a "practical" dependently-typed language, check out Idris:

http://www.idris-lang.org/