Topic: comment in functor.lean
Johan Commelin (Dec 22 2018 at 06:42):
Do I understand correctly that this comment is no longer accurate?
I think it refers to behaviour of an older version of
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