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 cjfd on Wednesday August 07, 2019 @05:09AM (#20633051)
Yes, I came here to say precisely that. It looks like it has about the same things available as coq as far as syntax is concerned, so what are the differences?
[ Parent | on HN ]
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by ocfnash on Wednesday August 07, 2019 @05:23AM (#20633106)
Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC.

For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features (not true in CIC).

It would just be nice to see a list of the rules.

Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.

[ Parent | on HN ]