The type system of Idris is similar to the one used by Agda and theorem-proving in it is similar to Coq, including tactics.
Sistemul de tip Idris este similar celui folosit de Agda și teorema-dovedind în el este similar cu Coq, inclusiv tactici.