Skip to content

feat: make Quot live in Sort (max 1 u) rather than Sort u - #15023

Draft
arthur-adjedj wants to merge 2 commits into
leanprover:masterfrom
arthur-adjedj:fixQuot2
Draft

feat: make Quot live in Sort (max 1 u) rather than Sort u#15023
arthur-adjedj wants to merge 2 commits into
leanprover:masterfrom
arthur-adjedj:fixQuot2

add test doc comment

27291ba
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-awaiting-mathlib
succeeded Sep 4, 2026 in 3s