Zulip Chat Archive

Stream: maths

Topic: comment in functor.lean


view this post on Zulip Johan Commelin (Dec 22 2018 at 06:42):

Do I understand correctly that this comment is no longer accurate?
https://github.com/leanprover/mathlib/blob/master/category_theory/functor.lean#L28-L29
I think it refers to behaviour of an older version of restate_axiom.

view this post on Zulip Johan Commelin (Dec 22 2018 at 06:47):

@Scott Morrison :up:

view this post on Zulip Scott Morrison (Dec 22 2018 at 06:49):

That's right, the comment needs updating.


Last updated: May 12 2021 at 06:14 UTC