leanprover-community / mathlib

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

Zulip Chat Archive

Stream: PR reviews

Topic: Data.Dlist !4#1498


Ruben Van de Velde (Apr 14 2023 at 09:00):

Do we want to port dlist at all?

Eric Wieser (Apr 14 2023 at 10:38):

I assume the thing to do for now is just ignore files like this in favor of more important ones, until they reach the top of the dashboard and we actually have to decide


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll