agda-stdlib

It'd be more like decideValidity : (p : A -> Type) -> (a : A) -> Either (p a) (Not (p a)) and for some classes of propositions this is a really useful type, e.g. the notion of decidable equality[0]. For general propositions you're talking about unbounded proof search, however. Undecidable propositions will fail to terminate (thus causing problems in a total language). Decidable propositions may still be exponentially slow to decide. Some classes of propositions may be known to be decidable, but knowing generally whether or not a proposition is undecidable is undecidable (Halting). [0] https://github.com/agda/agda-stdlib/blob/master/src/Relation...

I find Idris has a more computational flair while Agda is often "done after typechecking". Idris doesn't enforce termination as strictly as Agda. Idris' interactive modes are less friendly and powerful—Agda's emacs mode is best in breed. Idris has typeclasses and Agda something akin to first-class modules (as stated above). That's a fairly big difference. Idris handles laziness and strictness (or, relatedly, data/codata) a little differently than Agda, but it's not a huge concern until you get technical. Idris is also just younger than Agda and subsequently works a little wonkily. Again I find this exposed through the interactive mode which sometimes provides rather strange information. Although honestly that happens in both Agda and Idris. Idris has nice syntax for embedded DSLs which is demonstrated in its Effects library which would be