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.

Sign up for GitHub

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

Jump to bottom

Lean: fix indentation of match blocks #966

Merged
merged 1 commit into from
Feb 11, 2025
Merged

Lean: fix indentation of match blocks #966

merged 1 commit into from
Feb 11, 2025

Conversation

javra
Copy link
Collaborator

@javra javra commented Feb 10, 2025

No description provided.

@javra javra force-pushed the lean/match-indent branch from b3d3655 to 6e21d15 Compare February 10, 2025 16:23
@github-actions GitHub Actions
Copy link

github-actions bot commented Feb 10, 2025 •
edited
Loading

Test Results

   12 files  ±0     25 suites  ±0   0s ⏱️ ±0s
  764 tests ±0    764 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 708 runs  ±0  2 708 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit 68f5ddf. ± Comparison against base commit b689188.

♻️ This comment has been updated with latest results.

@javra javra force-pushed the lean/match-indent branch from 6e21d15 to ffa3317 Compare February 10, 2025 16:59
@tobiasgrosser tobiasgrosser added the Lean Issues with Sail to Lean translation label Feb 10, 2025
@javra javra force-pushed the lean/match-indent branch from ffa3317 to 68f5ddf Compare February 11, 2025 10:08
@bacam bacam merged commit 40d03c0 into rems-project:sail2 Feb 11, 2025
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ineol ineol ineol approved these changes

@lfrenot lfrenot lfrenot approved these changes

Assignees
No one assigned
Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@javra @ineol @lfrenot @tobiasgrosser @bacam