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: Feb 28 2026 at 14:05 UTC

Theme Simple by wildflame © 2016 Powered by jekyll