Commit 2023-11-25 15:15 1c6e8b59
View on Github →chore: Fix universe (misprint in Portmanteau.lean). (#8620)
In my earlier PR #8097 there there was a typo variable {Ω : Type} which should have been a universe polymorphic variable {Ω : Type*}. This PR fixes 1 character. Apologies!