fix: make sure `#check id` heeds `pp.raw`

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

fix: make sure `#check id` heeds `pp.raw` #6181

Closed kmill closed 6 days ago

kmill commented 6 days ago

This PR fixes a bug where the signature pretty printer would ignore the current setting of pp.raw. This fixes an issue where #check ident would not heed pp.raw. Closes #6090.

leanprover-community-bot commented 6 days 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 5145030ff4bed884213f584f8b2402be82e96d45 --onto 6202461a21d2636129cb8950cd9b6549ccf4b185. (2024-11-23 00:43:49)