> Even though Idris is marketed for “practical programming” it doesn’t have partial functions!! Both Idris and Agda have partial functions. Idris uses a keywor

> Even though Idris is marketed for “practical programming” it doesn’t have partial functions!! Both Idris and Agda have partial functions. Idris uses a keyword "partial", and Agda uses a pragma "NON_TERMINATING".