Zulip Chat Archive
Stream: mathlib4
Topic: what's the n argument for Repr.reprPrec?
Arien Malec (Jan 15 2023 at 00:13):
In docs4#Repr reprPrec is α → Nat → Lean.Format -- what does then represent?
Eric Wieser (Jan 15 2023 at 00:35):
It's the precedence
Eric Wieser (Jan 15 2023 at 00:37):
So that it can insert parens as needed
Last updated: Dec 20 2023 at 11:08 UTC