Skip to content
Check PR title for commit convention

fix: handle dot notation on local variables in grind parameters #33723

Sign in to view logs

fix: handle dot notation on local variables in grind parameters

fix: handle dot notation on local variables in grind parameters #33723

Triggered via pull request December 10, 2025 04:08
@kim-emkim-em
opened #11573
fix-grind-dot-notation-params
Status Failure
Total duration 10s
Artifacts –

pr-title.yml

on: pull_request
check-pr-title
5s
check-pr-title
Fit to window
Zoom out
Zoom in

Annotations

1 error
check-pr-title
PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).