Zulip Chat Archive

Stream: general

Topic: leftover trace?


view this post on Zulip Patrick Massot (Sep 29 2018 at 20:50):

When I build mathlib, I see:

view this post on Zulip Patrick Massot (Sep 29 2018 at 20:50):

@[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

view this post on Zulip Patrick Massot (Sep 29 2018 at 20:50):

Is there a debug trace left somewhere?

view this post on Zulip Simon Hudon (Sep 29 2018 at 23:01):

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


Last updated: May 14 2021 at 22:15 UTC