Skip to content

Add unreachable in the STLC language - #72

Merged
petros-marko merged 3 commits into
mainfrom
unreachable-expr
Jul 18, 2026
Merged

Add unreachable in the STLC language#72
petros-marko merged 3 commits into
mainfrom
unreachable-expr

Conversation

@petros-marko

Copy link
Copy Markdown
Collaborator

Add unreachable to the language, it doesn't reduce, and it type checks against anything as long as False is provable.

@petros-marko

Copy link
Copy Markdown
Collaborator Author

@jam-khan take a look when you get a chance.

Comment thread Flex/VCG/STLC/Examples.lean Outdated
@petros-marko
petros-marko requested a review from nilehmann July 17, 2026 23:01
@jam-khan

Copy link
Copy Markdown
Owner

@petros-marko there are some conflicts, but overall PR looks good

@petros-marko
petros-marko merged commit 6bc56e2 into main Jul 18, 2026
2 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.

3 participants