Skip to content

[Merged by Bors] - chore: use notation3 for Ordinal.typeLT#39798

Closed
vihdzp wants to merge 2 commits into
leanprover-community:masterfrom
vihdzp:typelt
Closed

[Merged by Bors] - chore: use notation3 for Ordinal.typeLT#39798
vihdzp wants to merge 2 commits into
leanprover-community:masterfrom
vihdzp:typelt