chore: turn off pp.mvars in apply? results

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 kim-em closed 1 week ago

kim-em commented 1 week ago

Per request on zulip.

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 405593ea28846014c59d73ae1fd0c438a0660811 --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 00:37:10)