## Stream: maths

### Topic: comment in functor.lean

#### 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.

#### Johan Commelin (Dec 22 2018 at 06:47):

@Scott Morrison :up:

#### Scott Morrison (Dec 22 2018 at 06:49):

That's right, the comment needs updating.

Last updated: May 12 2021 at 06:14 UTC