Zulip Chat Archive

Stream: general

Topic: tactic.basic


view this post on Zulip Johan Commelin (May 17 2019 at 06:28):

Is rw not exported by tactic.basic?
https://github.com/leanprover-community/mathlib/pull/1029/files/db3ffb7e548eb029e3b0fe99a804da5814a983d6..8593748a45c98b2fdbf2c99562d5b312f9289bca#diff-af7a83126ec31af486624837502fb79eR8
That seems like a mistake...

view this post on Zulip Keeley Hoek (May 17 2019 at 06:31):

Wouldn't that probably be for assoc_rw?

view this post on Zulip Johan Commelin (May 17 2019 at 06:31):

What do you mean?

view this post on Zulip Keeley Hoek (May 17 2019 at 06:32):

assoc_rw is defined in https://github.com/leanprover-community/mathlib/blob/master/src/tactic/rewrite.lean, that's why you need the import

view this post on Zulip Keeley Hoek (May 17 2019 at 06:32):

(I think)

view this post on Zulip Kevin Buzzard (May 17 2019 at 06:33):

rw must be in core because it's in TPIL

view this post on Zulip Keeley Hoek (May 17 2019 at 06:34):

Oh sorry I misunderstood what you meant Johan.

view this post on Zulip Keeley Hoek (May 17 2019 at 06:34):

Sure, totally, that makes sense

view this post on Zulip Johan Commelin (May 17 2019 at 06:39):

#1039 — Let's see if Travis is happy.

view this post on Zulip Johan Commelin (May 17 2019 at 06:39):

I also sorted the list of imports


Last updated: May 14 2021 at 23:14 UTC