Skip to content

fixup: comprehension coproducts introduction rule#609

Merged
plt-amy merged 1 commit intothe1lab:mainfrom
ncfavier:comp-coproducts-intro
Mar 31, 2026
Merged

fixup: comprehension coproducts introduction rule#609
plt-amy merged 1 commit intothe1lab:mainfrom
ncfavier:comp-coproducts-intro

Conversation

@ncfavier
Copy link
Copy Markdown
Member

The rule as currently written is the introduction rule for Π-types.

@ncfavier ncfavier requested a review from TOTBWF March 22, 2026 16:41
@Lavenza
Copy link
Copy Markdown
Member

Lavenza commented Mar 22, 2026

Pull request preview

Changed pages

@plt-amy plt-amy force-pushed the comp-coproducts-intro branch from 6108f26 to f3fe4ca Compare March 22, 2026 18:33
Copy link
Copy Markdown
Collaborator

@TOTBWF TOTBWF left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for fixing this!

@TOTBWF TOTBWF force-pushed the comp-coproducts-intro branch from f3fe4ca to d15d85a Compare March 28, 2026 17:36
@plt-amy plt-amy force-pushed the comp-coproducts-intro branch from d15d85a to d58f1da Compare March 29, 2026 19:50
@plt-amy plt-amy force-pushed the comp-coproducts-intro branch from d58f1da to 48a52ca Compare March 31, 2026 19:08
@plt-amy plt-amy enabled auto-merge (squash) March 31, 2026 19:09
@plt-amy plt-amy merged commit 30986d9 into the1lab:main Mar 31, 2026
3 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.

4 participants