Commit 2026-07-24 07:15 c89fc4be
View on Github →chore: add missing noncomputable (#41446)
All these definitions are noncomputable (because they use choice/produce sets), but the computability checker doesn't spot this until I try making Set a one-field structure. This is because the computability checker doesn't even try to compute sorts, but it doesn't see that s : Set α is (equivalent to) a family of sorts.