Skip to content

Added conclude by contradiction construction#34

Merged
PatrickMassot merged 3 commits into
PatrickMassot:masterfrom
impermeable:feature/conclude-by-contradiction
Jun 8, 2026
Merged

Added conclude by contradiction construction#34
PatrickMassot merged 3 commits into
PatrickMassot:masterfrom
impermeable:feature/conclude-by-contradiction

Conversation

@pimotte

@pimotte pimotte commented May 13, 2026

Copy link
Copy Markdown
Contributor

Fixes #31

We are a little bit further in formalizing some exercises for our introduction to proofs course, and we really do want to have this. If you prefer to have it scoped, I'm happy to set that up too.

I'm also not entirely sure about what the deal is with whitespace/division into strings for elab rules, so I might have done something silly there.

@PatrickMassot

Copy link
Copy Markdown
Owner

I think the string division stuff in this file is a historical accident which is no longer necessary. But you don’t have to fix it in this PR, being consistent with the surrounding syntax declarations is good.

Please scope those new syntax if this is isn’t causing too much trouble for you because I’m really not convinced this is generally useful (and, as every new syntax, it introduces new parser confusion potential).

@PatrickMassot
PatrickMassot merged commit ee25c68 into PatrickMassot:master Jun 8, 2026
1 check 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.

Language proposal: Arriving at a contradiction

2 participants