Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Duplicate definitions in different code files #5

Open
ShreckYe opened this issue Jul 9, 2021 · 1 comment
Open

Duplicate definitions in different code files #5

ShreckYe opened this issue Jul 9, 2021 · 1 comment
Assignees

Comments

@ShreckYe
Copy link

ShreckYe commented Jul 9, 2021

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
Copy link

sxhya commented Mar 22, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants