Skip to content

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

fix: handle dot notation on local variables in grind parameters

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

Triggered via pull request December 10, 2025 04:08
Status Success
Total duration 6s
Artifacts

awaiting-mathlib.yml

on: pull_request
check-awaiting-mathlib
2s
check-awaiting-mathlib
Fit to window
Zoom out
Zoom in