Skip to content

Conversation

@joscoh
Copy link
Contributor

@joscoh joscoh commented Oct 23, 2025

Issue #, if available:

Description of changes:

Redefines an Identifier as String x IDMeta and parameterizes LExpr, LExprT, etc with IDMeta rather than Identifier. This allows several important operations on identifiers and expressions including:

  • Generating arbitrary distinct identifiers (assuming IDMeta is Inhabited)
  • Pattern matching on the name of a .op expression

Note: since the ToFormat instance of BoogieIdent (the only non-String identifier in use) simply gave the name, this implementation ignores IDMeta when converting Identifiers to String or Format.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@atomb atomb enabled auto-merge October 23, 2025 21:15
@atomb atomb added this pull request to the merge queue Oct 24, 2025
Merged via the queue into main with commit 4da203b Oct 24, 2025
10 checks passed
@atomb atomb deleted the josh/identifier branch October 24, 2025 20:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants