alt Hacker NewsI'm not sure you prefer Agda so much as you prefer providing proof terms functionally rather than imperatively. Then again I've never used Agda; how does it differ from Coq/Rocq minus Ltac or Lean minus tactics?
I'm not sure you prefer Agda so much as you prefer providing proof terms functionally rather than imperatively. Then again I've never used Agda; how does it differ from Coq/Rocq minus Ltac or Lean minus tactics?
Coq has much less support for working with dependent types; you need lots of annotations compared to Agda (which has superior dependent pattern matching support). Lean is somewhere between the two.