lean4-htt/stage0
Sebastian Graf 82c35eb517
refactor: rename goalDotAlt/goalCaseAlt to invariantDotAlt/invariantCaseAlt (#13160)
This PR renames `goalDotAlt` to `invariantDotAlt` and `goalCaseAlt` to
`invariantCaseAlt` to better reflect that these syntax nodes are
specific
to invariant alternatives in `mvcgen`, not general goal alternatives.

Part 2 of #13137, which made `elabInvariants` resilient to this rename
by using positional dispatch instead of quotation pattern matching.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-27 16:01:32 +00:00
..
src refactor: rename goalDotAlt/goalCaseAlt to invariantDotAlt/invariantCaseAlt (#13160) 2026-03-27 16:01:32 +00:00
stdlib chore: update stage0 2026-03-27 15:17:24 +00:00