Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains. Parent comment
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.
There are no comments on this comment yet.
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.