Skip to content

Clean-ups to Spaces/Int/ and Spaces/Pos/#1870

Merged
jdchristensen merged 2 commits intoHoTT:masterfrom
jdchristensen:Int-Pos
Feb 24, 2024
Merged

Clean-ups to Spaces/Int/ and Spaces/Pos/#1870
jdchristensen merged 2 commits intoHoTT:masterfrom
jdchristensen:Int-Pos

Commits

Commits on Feb 24, 2024