pp.raw not affecting signature printing

Description

Using pp.raw to debug issues related to types doesn’t work as expected.

Steps to Reproduce

With set_option pp.raw true I’d expect to see all the gory details below, but #check doesn’t seem to heed it, and #print doesn’t seem to heed it when printing signatures.

def foo : Nat → Nat
 | 0 => 0
 | n => n

set_option pp.raw true

/-- info: foo : Nat → Nat -/
#guard_msgs in
#check foo

/-- info: id.{1} (Nat -> Nat) foo : Nat -> Nat -/
#guard_msgs in
#check id (@foo)

/--
info: def foo : Nat -> Nat :=
fun (x._@._hyg.7 : Nat) => foo.match_1.{1} (fun (x._@._hyg.7.18 : Nat) => Nat) x._@._hyg.7 (fun (_ : Unit) => OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (fun (n : Nat) => n)
-/
#guard_msgs in
#print foo

/-- info: Bool.true : Bool -/
#guard_msgs in
#check true

/-- info: constructor Bool.true : Bool -/
#guard_msgs in
#print true

Expected behavior: [Clear and concise description of what you expect to happen]

Actual behavior: [Clear and concise description of what actually happens]

Versions

Lean 4.15.0-nightly-2024-11-15 Target: x86_64-unknown-linux-gnu

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

leanprover / lean4