leftover trace?

Stream: general

[Patrick Massot]

When I build mathlib, I see:

[Patrick Massot]

@[class, priority 100, to_additive name.mk_string "add_group" name.anonymous]
structure group : Type u → Type u
fields:
group.mul : Π {α : Type u} [c : group α], α → α → α
group.mul_assoc : ∀ {α : Type u} [c : group α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
group.one : Π (α : Type u) [c : group α], α
group.one_mul : ∀ {α : Type u} [c : group α] (a : α), 1 * a = a
group.mul_one : ∀ {α : Type u} [c : group α] (a : α), a * 1 = a
group.inv : Π {α : Type u} [c : group α], α → α
group.mul_left_inv : ∀ {α : Type u} [c : group α] (a : α), a⁻¹ * a = 1

[Patrick Massot]

Is there a debug trace left somewhere?

[Simon Hudon]

You can use grep on the mathlib directory. It's probably one of the flavors of #print