even 1.5 yrs after switching to Coq, I still find myself complain about how clunky it is to write dependently typed functions that are meant to be computed.
in other words, Coq is the Java of dependent types. it is the industry standard but it'd make a beginner hate dep't types.
Quote Tweet
Some #Coq users wonder how can #Agda be usable without tactics. They forget that Agda's dependent pattern matching *is* a powerful tactic.
Show this thread
2
13
91
