4 ms·
Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't
by siknad 3y ago
Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
- epgui 3y agoYou may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).