Zulip Chat Archive

Stream: general

Topic: dsimp; simp


view this post on Zulip 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

view this post on Zulip Chris Hughes (Nov 03 2018 at 21:55):

Can we make a dsimp and simp all in one tactic.

view this post on Zulip 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). :-)

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:33):

@Scott Morrison I think we should expand the category theory library

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:33):

instead of saying that Lean is not ready for it

view this post on Zulip Scott Morrison (Nov 03 2018 at 22:34):

Absolutely, I agree it should be expanded massively.


Last updated: May 07 2021 at 00:30 UTC