4 ms·
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?
by cjfd 7y ago
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?
- ocfnash 7y agoWell 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 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.