Thanks! And what about agda and Idris? | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

The_rationalist on April 6, 2020 | parent | context | favorite | on: Doing a math assignment with the Lean theorem prov...

Thanks! And what about agda and Idris?

aweinstock on April 6, 2020 [–]

Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact