Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: ideas for exercises
Jalex Stark (May 17 2020 at 16:30):
using rw under a universal quantifier should "just" require introing and reverting
Last updated: Dec 20 2023 at 11:08 UTC
using rw under a universal quantifier should "just" require introing and reverting
Last updated: Dec 20 2023 at 11:08 UTC