Skip to content

Test: evil recursors making true equalities false - #156

Merged
nomeata merged 2 commits into
leanprover:masterfrom
robsimmons:large-elim-prop-bool
Aug 25, 2026
Merged

Test: evil recursors making true equalities false#156
nomeata merged 2 commits into
leanprover:masterfrom
robsimmons:large-elim-prop-bool

Conversation

@robsimmons

@robsimmons robsimmons commented Aug 24, 2026

Copy link
Copy Markdown
Contributor

I think I finally understand what #49 was doing — or rather, I understand this test case, and my friendly robot tells me it's similar to what #49 was doing.

Captures an issue with kiota that isn't currently exercised. Fails for rpylean because rpylean accepts bad recursors.

@nomeata nomeata closed this Aug 25, 2026
@nomeata nomeata reopened this Aug 25, 2026
@nomeata
nomeata enabled auto-merge (squash) August 25, 2026 06:08
@nomeata
nomeata merged commit 0dfcffe into leanprover:master Aug 25, 2026
44 of 46 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.

2 participants