Zulip Chat Archive

Stream: lean4

Topic: Missing `@[expose]`

Robert Maxton (Dec 10 2025 at 04:02):

Is docs#decidable_of_bool meant to be an @[expose]ed def like its siblings? It doesn't have one; should I just make a PR?

Sebastian Ullrich (Dec 10 2025 at 09:38):

That sounds sensible to me, yes

Robert Maxton (Dec 12 2025 at 01:53):

Sebastian Ullrich said:

That sounds sensible to me, yes

https://github.com/leanprover/lean4/pull/11625
Unsure how much of the RFC/PR process I should be doing for an edit this small

Junyan Xu (Dec 12 2025 at 17:56):

Could someone take a look at https://github.com/leanprover/lean4/pull/11401 ?

Last updated: Dec 20 2025 at 21:32 UTC