Zulip Chat Archive
Stream: general
Topic: erw in conv
Reid Barton (Nov 13 2018 at 02:37):
Is it intentional that you have to import tactic.converter.interactive to get the new conv goodies?
Reid Barton (Nov 13 2018 at 02:55):
It's not mentioned in the docs
Keeley Hoek (Nov 13 2018 at 03:00):
That's true, it should be
I just put them where the already existing extras were
But you'll always have to import something
Last updated: Dec 20 2023 at 11:08 UTC