Skip to content

Add imax right-successor corner cases - #176

Merged
nomeata merged 1 commit into
leanprover:masterfrom
phiferd:imax-right-successor-corner-cases
Aug 30, 2026
Merged

Add imax right-successor corner cases#176
nomeata merged 1 commit into
leanprover:masterfrom
phiferd:imax-right-successor-corner-cases

Conversation

@phiferd

@phiferd phiferd commented Aug 29, 2026

Copy link
Copy Markdown
Contributor

Closes #175.

Adds the two requested universe-normalization corner cases:

  • imax u 1 versus max u 1
  • imax u (v + 1) versus max u (v + 1)

They are a single corner-cases/ export with outcome: either: a checker may
reject the hand-crafted declarations conservatively, or accept them using more
complete level normalization. The official checker rejects the export and
Arena records that result as permitted rather than scoring it as a failure.

Validation:

  • .venv-arena/bin/python ./lka.py build-test corner-cases/imax-right-successor
  • .venv-arena/bin/python ./lka.py run --checker official --test corner-cases/imax-right-successor

@phiferd
phiferd marked this pull request as ready for review August 29, 2026 16:24
@nomeata

nomeata commented Aug 29, 2026

Copy link
Copy Markdown
Collaborator

I don't want to blame checkers that already implement a more complete level normalization. So these tests probably shouldn't be tutorial tests, but go into the corner-cases/ group, with expected: either

@phiferd
phiferd force-pushed the imax-right-successor-corner-cases branch from 34407be to 7333a62 Compare August 29, 2026 23:45
@nomeata
nomeata enabled auto-merge (squash) August 30, 2026 08:54
@nomeata
nomeata merged commit 9a4bf18 into leanprover:master Aug 30, 2026
25 checks passed
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.

Add reject coverage for imax right-successor comparisons

2 participants