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: Dec 20 2023 at 11:08 UTC