News for hackers. Stuff that matters.

A comment on Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains. Parent comment

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Blaisorblade0 on Sunday August 11, 2019 @07:13AM (#20667594)
Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by dllthomas on Sunday August 11, 2019 @12:55PM (#20669041)
I'm not sure I can name another language with coherence, dependant types or not. To be fair, even GHC is half-hearted about it.
[ Parent | on HN ]