Zulip Chat Archive

Stream: general

Topic: tactic.basic

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

Keeley Hoek (May 17 2019 at 06:31):

Wouldn't that probably be for assoc_rw?

Johan Commelin (May 17 2019 at 06:31):

What do you mean?

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

Keeley Hoek (May 17 2019 at 06:32):

(I think)

Kevin Buzzard (May 17 2019 at 06:33):

rw must be in core because it's in TPIL

Keeley Hoek (May 17 2019 at 06:34):

Oh sorry I misunderstood what you meant Johan.

Keeley Hoek (May 17 2019 at 06:34):

Sure, totally, that makes sense

Johan Commelin (May 17 2019 at 06:39):

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

Johan Commelin (May 17 2019 at 06:39):

I also sorted the list of imports

Last updated: Dec 20 2023 at 11:08 UTC