search

arend-lang / tutorial-code

Source code & exercises in Arend's documentation
https://arend-lang.github.io/documentation/tutorial
Apache License 2.0
21 stars 9 forks source link

Duplicate definitions in different code files #5

Open ShreckYe opened 3 years ago

ShreckYe commented 3 years ago

There are a lot of duplicate copied definitions in various code files, such as those of Empty, Unit, Bool, List, =, <, etc., and their related functions. This makes related implemented functions (proven propositions) not reusable, so when completing the exercises in different files it's necessary to copy and paste the needed ones and produce more duplicate definitions. This makes the code unnecessarily long and redundant. Would it be better to remove such duplicate definitions and just import the needed ones in appropriate places?

sxhya commented 1 year ago

I totally agree with the author of the issue. Do not repeat basic definitions a hundred times such as Empty Unit, absurd, List, Bool etc from lesson to lesson. This only confuses navigation. List alone is repeated in the library at least 5 times. Bool at least 2 times. Case.ard has its own + and *, and Basics.ard has its own +. By the way, currently, Arend completion does not show which definition is imported from where, so it is very easy to get confused in the long list of identical definitions. It's best to leave one copy of each definition in Basics.ard. Even better tutorial- code could depend on arend-lib and reuse definitions from there, so that all definitions from Basics would be commented out.