separating constructive maths from non-constructive maths

Stream: new members

[Robert Watson]

Hi there, I want to make sure my lean code and proofs are such that I have any nonconstructive proofs or non-computable functions separate from constructive proofs and computable functions. I am aware that you can specifically label functions non-computable and introduce explicitly a classical locale to allow 'normal' maths flexibility (which is great). But equally I am concerned that when I want everything constructive and/or computable that I might be importing something that uses non-computability or non-constructive proofs accidentally. How does Lean (3 and 4 if they are different!) handle this?

[Martin Dvořák]

I wish I knew!

[Henrik Böving]

You can ensure this manually by using #print axioms declName I guess it could also be turned into an automatic sort of thing as a meta program in Lean 4 rather easily.

[Yaël Dillies]

DId we end up implementing @[intuit]?