My understanding is that Agda puts much less emphasis on general programming. It's more focused on proving.