Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

refactor(*): refactor associates#710

Merged
ChrisHughes24 merged 1 commit into
masterfrom
associates-refactor
Feb 10, 2019
Merged

refactor(*): refactor associates#710
ChrisHughes24 merged 1 commit into
masterfrom
associates-refactor

Conversation

@kckennylau

Copy link
Copy Markdown
Collaborator

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@ChrisHughes24
ChrisHughes24 merged commit 9b28db0 into master Feb 10, 2019
@ChrisHughes24
ChrisHughes24 deleted the associates-refactor branch February 12, 2019 01:55
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants