refactor: lake: avoid `v!` in builtin code

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

Closed tydeu closed 1 week ago

tydeu commented 1 week ago

Use of v! in Lake code can cause bootstrapping failures and is easily avoided. It is perfectly safe in user code.

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6073 has successfully built against this PR. (2024-11-14 02:21:48) View Log