Commit 2025-08-20 12:55 691373ca
View on Github →feat: extensionality for normal functions (#28677)
Two normal functions are equal when they're equal on 0 and on successors.
This also gets rid of one of the last uses of Ordinal.bsup.
feat: extensionality for normal functions (#28677)
Two normal functions are equal when they're equal on 0 and on successors.
This also gets rid of one of the last uses of Ordinal.bsup.