Skip to content

refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual#3077

Merged
nomeata merged 1 commit intomasterfrom
joachim/unpack-funcs
Dec 18, 2023
Merged

refactor: move unpackArg etc. to WF.PackDomain/WF.PackMutual#3077
nomeata merged 1 commit intomasterfrom
joachim/unpack-funcs

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Dec 15, 2023

extracted from #3040 to keep the diff smaller

@nomeata nomeata added the will-merge-soon …unless someone speaks up label Dec 15, 2023
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 15, 2023
@ghost
Copy link
Copy Markdown

ghost commented Dec 15, 2023

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-15 15:01:31)

@nomeata nomeata added this pull request to the merge queue Dec 18, 2023
Merged via the queue into master with commit 7acbee8 Dec 18, 2023
@nomeata nomeata deleted the joachim/unpack-funcs branch December 18, 2023 14:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant