A huge overlap. Idris is aimed at being a general purpose language with proof assistant characteristics while some of its peers are more theorem provers built with general purpose language characteristics.