Skip to content

[#14462] chore: rename Nat.div_eq to Nat.div_eq_ite#6

Merged
downstream-lean4[bot] merged 3 commits into
masterfrom
adaptation-14462
Jul 22, 2026
Merged

[#14462] chore: rename Nat.div_eq to Nat.div_eq_ite#6
downstream-lean4[bot] merged 3 commits into
masterfrom
adaptation-14462

Conversation

@downstream-lean4

Copy link
Copy Markdown
Contributor

This is the adaptation PR for leanprover/lean4#14462.

@downstream-lean4 downstream-lean4 Bot added the adaptation This is an adaptation PR for a PR in the lean4 repository. label Jul 20, 2026
@downstream-lean4

Copy link
Copy Markdown
Contributor Author

Build Report

For commit downstream: follow upstream PR

Repo Critical Build Test Lint
mathlib4 ✅ in 19m 🟥 in 1m ✅ in 1m
verso-slides 🟥 in 0m ⏭️ ⏭️
Green repos
Repo Critical Build Test Lint
aesop ✅ in 0m ✅ in 0m ⏭️
batteries ✅ in 0m ✅ in 0m ✅ in 0m
import-graph ✅ in 0m ✅ in 0m ⏭️
lean4-cli ✅ in 0m ✅ in 0m ⏭️
plausible ✅ in 0m ✅ in 0m ⏭️
ProofWidgets4 ✅ in 0m ✅ in 0m ⏭️
quote4 ✅ in 0m ✅ in 0m ⏭️
reference-manual ✅ in 1m ⏭️ ⏭️
BibtexQuery ✅ in 0m ⏭️ ⏭️
comparator ✅ in 0m ⏭️ ⏭️
cslib ✅ in 1m ✅ in 0m ✅ in 0m
doc-gen4 ✅ in 0m ⏭️ ⏭️
illuminate ✅ in 0m ✅ in 0m ⏭️
lean4-unicode-basic ✅ in 0m ✅ in 0m ⏭️
lean4export ✅ in 0m ✅ in 0m ⏭️
LeanSearchClient ✅ in 0m ✅ in 0m ⏭️
leansqlite ✅ in 0m ✅ in 0m ⏭️
repl ✅ in 0m ✅ in 0m ⏭️
verso ✅ in 2m ✅ in 1m ⏭️
verso-web-components ✅ in 0m ⏭️ ⏭️

View run

@downstream-lean4
downstream-lean4 Bot merged commit 28e1767 into master Jul 22, 2026
1 check failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

adaptation This is an adaptation PR for a PR in the lean4 repository.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant