leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

Closed mhuisi closed 1 week ago

mhuisi commented 1 week ago

5835 contains a brittle test that uses an FVar ID, which caused a failure on master. This PR changes that test to use a declaration instead.

leanprover-community-bot commented 1 week 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 4bef3588b592c1cdcba190ef9bcd92b05fd5cbb7 --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-19 10:17:28)