Zulip Chat Archive

Stream: mathlib4

Topic: Topology.Tactic

Yury G. Kudryashov (Jan 25 2023 at 23:00):

Are there any volunteers to write the continuity tactic or teach me how to write it?

Heather Macbeth (Jan 25 2023 at 23:19):

This is a wrapper on top of apply_rules and I've been doing a lot of those lately. I'd be happy to try, but can't before the weekend, so someone else should jump in first if available.

Yury G. Kudryashov (Jan 25 2023 at 23:57):

Can you point me at an example so that I can try to copy+edit?

Heather Macbeth (Jan 26 2023 at 00:17):

This folder in lecture notes for a course:
https://github.com/hrmacbeth/math2001/tree/main/Math2001/Tactic/Rel
and also this PR: mathlib4#1740

Last updated: Dec 20 2023 at 11:08 UTC