Skip to content

Conversation

@leodemoura
Copy link
Member

This PR implements a compact notation for inspecting the grind state in interactive mode. Within a grind tactic block, each tactic may optionally have a suffix of the form | filter?.

Examples:

instantiate | gen > 0  -- Displays terms in the `grind` state after executing `instantiate` with generation greater than zero
instantiate |  -- Displays the `grind` state after executing `instantiate`

Remark: If the user places the cursor one space before |, the state before executing instantiate is displayed.
This PR removes the code that was silently displaying the grind state after each tactic step, as it was too noisy.
It also updates the notation for the first combinator in the grind tactic mode to avoid conflicts with the new syntax.

@leodemoura leodemoura requested a review from kim-em as a code owner October 17, 2025 19:42
@leodemoura leodemoura added the changelog-tactics User facing tactics label Oct 17, 2025
@leodemoura leodemoura enabled auto-merge October 17, 2025 19:42
@leodemoura leodemoura added this pull request to the merge queue Oct 17, 2025
Merged via the queue into master with commit c76411d Oct 17, 2025
19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants