Skip to content

Conversation

@leodemoura
Copy link
Member

This PR implements hover information for grind anchors. Anchors are stable hash codes for referencing terms in the grind state. The anchors will be used when auto generating tactic scripts. The hover display the following information:

1- In the instantiate tactic, it displays the type of the theorem being instantiated.
image

2- In the cases tactic, the hover information depends on the kind of case-split.
a) Proposition
image

b) A hypotheses. In this case, you can opt to replace the anchor with the hypothesis' name if it is accessible.
image

c) A term. The hover displays just the type, by grind logs a silent information with additional information

image

@leodemoura leodemoura requested a review from kim-em as a code owner October 15, 2025 02:41
@leodemoura leodemoura added the changelog-tactics User facing tactics label Oct 15, 2025
@leodemoura leodemoura enabled auto-merge October 15, 2025 02:41
@leodemoura leodemoura added this pull request to the merge queue Oct 15, 2025
Merged via the queue into master with commit 746206c Oct 15, 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