search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

Reorder declarations in Prelude.ard #292

Closed marat-rkh closed 3 years ago

marat-rkh commented 3 years ago

All the declarations in Prelude can be divided into 2 categories:

  1. Numbers
  2. Things related to paths and equality.

For some reason, I, Path, =, idp, and @ are defined before numbers, but coe, coe2, and iso are defined after. I think it would be more logical to put coe, coe2, and iso before numbers.

ice1000 commented 3 years ago

https://github.com/JetBrains/Arend/issues/250#issuecomment-666362789

Btw, I suggest problems related to Arend to go to https://github.com/JetBrains/Arend/issues.

marat-rkh commented 3 years ago

Oh, you are right, language repo is the right place for the issue. Thanks for moving!