Zulip Chat Archive
Stream: general
Topic: dsimp; simp
Reid Barton (Nov 03 2018 at 21:53):
I think I set a new personal record:
by dsimp [is_limit.equiv, adjunction.cone_equivalence]; simp; dsimp; simp
Chris Hughes (Nov 03 2018 at 21:55):
Can we make a dsimp and simp all in one tactic.
Scott Morrison (Nov 03 2018 at 22:32):
Yay, and I'm happy seeing is_limit.equiv being used moments after I wrote it (again). :-)
Kenny Lau (Nov 03 2018 at 22:33):
@Scott Morrison I think we should expand the category theory library
Kenny Lau (Nov 03 2018 at 22:33):
instead of saying that Lean is not ready for it
Scott Morrison (Nov 03 2018 at 22:34):
Absolutely, I agree it should be expanded massively.
Last updated: Dec 20 2023 at 11:08 UTC