refactor: allow `Sort u` in `Squash`

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 428 forks source link

Closed vihdzp closed 2 weeks ago

leanprover-community-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e55b681774494b1c5eebe9e506509e580b1f9d27 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 04:35:39)