Skip to content

Conversation

@haansn08
Copy link
Contributor

No description provided.

@DmxLarchey
Copy link
Collaborator

Hi @haansn08. Is this a systematic replacement of prodList by list_prod from StdLib?

@haansn08
Copy link
Contributor Author

@DmxLarchey Not sure what you mean by systematic, but I made sure the library still compiles.

@DmxLarchey
Copy link
Collaborator

@DmxLarchey Not sure what you mean by systematic, but I made sure the library still compiles.

I mean that there is no occurrence of prodList anymore after the resulting update? Or is this just a punctual change in two files ?

@haansn08
Copy link
Contributor Author

There are no other occurrences of prodList. I now also removed the Lemma prod_nil which also seems to be unused.

@DmxLarchey
Copy link
Collaborator

Considering it is a systematic replacement with an equivalent tool from the standard library, I would likely ok the change. @yforster and @mrhaandi do you agree with merging this ?

@DmxLarchey
Copy link
Collaborator

There are no other occurrences of prodList. I now also removed the Lemma prod_nil which also seems to be unused.

@DmxLarchey DmxLarchey closed this Oct 13, 2022
@DmxLarchey DmxLarchey reopened this Oct 13, 2022
@DmxLarchey
Copy link
Collaborator

There are no other occurrences of prodList. I now also removed the Lemma prod_nil which also seems to be unused.

If prod_nil isn't already in the StdLib, maybe it could be left.

@mrhaandi
Copy link
Collaborator

There are no other occurrences of prodList. I now also removed the Lemma prod_nil which also seems to be unused.

If prod_nil isn't already in the StdLib, maybe it could be left.

prod_nil refers to the removed prodList and should be removed as well. Since the equivalent statement for list_prod is not necessary, there is no need to formulate it.

@mrhaandi mrhaandi self-requested a review October 13, 2022 12:38
@mrhaandi
Copy link
Collaborator

I approve the proposed changes. @yforster it would be good to have a proper CI run before merge; what is the status of #171?

@mrhaandi
Copy link
Collaborator

To be on the safe side (without currently functioning ci), I have compiled the PR locally without issues.

@DmxLarchey DmxLarchey self-requested a review October 14, 2022 12:38
@mrhaandi mrhaandi merged commit b4c75f7 into uds-psl:coq-8.16 Oct 14, 2022
@haansn08 haansn08 deleted the prodLists branch October 14, 2022 13:14
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

Successfully merging this pull request may close these issues.

3 participants