Skip to content

Fix GetElem in Lean 4#2946

Merged
birkenfeld merged 1 commit intopygments:masterfrom
mdbrnowski:master
Feb 20, 2026
Merged

Fix GetElem in Lean 4#2946
birkenfeld merged 1 commit intopygments:masterfrom
mdbrnowski:master

Conversation

@mdbrnowski
Copy link
Copy Markdown
Contributor

I have added ]', ]?, and ]! as operators, since they are used as Data Lookups.

@birkenfeld
Copy link
Copy Markdown
Member

Fun-looking operators, but sure!

@birkenfeld birkenfeld merged commit c34f0c6 into pygments:master Feb 20, 2026
@Anteru Anteru added this to the 2.20.0 milestone Mar 26, 2026
@Anteru Anteru added the A-lexing area: changes to individual lexers label Mar 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

A-lexing area: changes to individual lexers

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants