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

doc: improve docstrings for repeat* tactics #4338

Merged
merged 1 commit into from
Jun 4, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Jun 4, 2024

No description provided.

@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 Jun 4, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f65e3ae9859a4288b94b4a9fda93f406244d8dbc --onto 81f5b07215b077f9b5be677f8689617512d3322c. (2024-06-04 01:23:20)

@semorrison semorrison added this pull request to the merge queue Jun 4, 2024
Merged via the queue into leanprover:master with commit e47d84e Jun 4, 2024
11 checks passed
Komyyy pushed a commit to Komyyy/lean4 that referenced this pull request Jun 4, 2024
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
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants