Zulip Chat Archive
Stream: lean4
Topic: spacing in #check Mul.mul
Kevin Buzzard (Jan 11 2024 at 12:04):
#check Mul.mul returns
Mul.mul.{u} {α : Type u} [self : Mul α] (a✝a✝¹ : α) : α
with no space between a✝ and a✝¹. Is this expected behaviour?
Last updated: May 02 2025 at 03:31 UTC