Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by js8 on Wednesday August 07, 2019 @05:09AM (#20633052)

I actually kinda like the idea. The concept of (limited set of) "reserved keywords" always annoyed the mathematical purist in me.

On an unrelated note, this-is-a-valid-identifier also in Lisp, but weirdly enough, the parens "( )" require shift. I think Lisp should use "[ ]" as parens because they do not require shift on modern keyboards.

[ Parent | on HN ]

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Sharlin on Wednesday August 07, 2019 @06:25AM (#20633403)

You mean, modern English keyboard layouts! Square brackets require alt(gr) on my keyboard. Seriously, most European layouts are ridiculously coding-unfriendly.

[ Parent | on HN ]

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by pmontra on Wednesday August 07, 2019 @07:22AM (#20633689)

Probably because coding was invented (and most of it still is) on an English keyboard.

I switch the layout of my non English keyboard in all coding windows and my fingers know what to press there.

[ Parent | on HN ]

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by cinnamonheart on Wednesday August 07, 2019 @01:34PM (#20636920)

Racket does allow usage of brackets and parentheses interchangeably, as far as I know:

    > [define [plus i j] [+ i j]]
    > [plus 1 2]
    3

[ Parent | on HN ]