Nobody said anything about "general-purpose functional programming languages", the blurb says "existing functional languages". All of Epigram, Agda and Coq are

Nobody said anything about "general-purpose functional programming languages", the blurb says "existing functional languages". All of Epigram, Agda and Coq are functional and currently exist. :) More seriously, Coq is designed explicitly to be a proof assistant, but Agda and Epigram are meant to be programming languages.