Skip to content

fix: docstrings for isplitl and isplitr - #687

Merged
MackieLoeffel merged 2 commits into
leanprover-community:masterfrom
ISTA-PLV:iSplitDocFix
Aug 31, 2026
Merged

MackieLoeffel merged 2 commits into
leanprover-community:masterfrom
ISTA-PLV:iSplitDocFix

Conversation

@alvinylt

Copy link
Copy Markdown
Contributor

Description

The functionalities described by the docstrings of isplit and isplitr are swapped.

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have added my name to the authors section of any appropriate files

@MackieLoeffel MackieLoeffel left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

Comment thread Iris/Iris/ProofMode/Tactics/Split.lean Outdated
Comment thread Iris/Iris/ProofMode/Tactics/Split.lean Outdated
Co-authored-by: Michael Sammler <MackieLoeffel@users.noreply.github.com>
@MackieLoeffel
MackieLoeffel merged commit 9f2723e into leanprover-community:master Aug 31, 2026
5 checks passed
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.

2 participants