leanprover-community / mathlib

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

Zulip Chat Archive

Stream: lean4

Topic: Filtering proof_n


Adam Topaz (Jun 10 2023 at 00:32):

Do we have some function, similar to, say docs4#Lean.Name.isInternal which also filters out things like docs4#toAddUnits.proof_1 ?

Scott Morrison (Jun 10 2023 at 00:57):

src4#Lean.Name.isBlackListed

Scott Morrison (Jun 10 2023 at 00:58):

although just src4#Lean.Name.isInternal' would suffice for your question.

Adam Topaz (Jun 10 2023 at 01:08):

Thanks!


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll