leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: PR reviews

Topic: !4#2145 continuity tactic


Moritz Doll (Feb 10 2023 at 09:40):

I would like to get this merged rather sooner than later, since it creates the attribute and otherwise we more work by commenting out the attribute and then coming back and reenabling it.


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll