# Zulip Chat Archive

## Stream: new members

### Topic: separating constructive maths from non-constructive maths

#### Robert Watson (Mar 12 2022 at 18:35):

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 (Mar 12 2022 at 18:39):

I wish I knew!

#### Henrik Böving (Mar 12 2022 at 18:46):

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 (Mar 12 2022 at 19:10):

DId we end up implementing `@[intuit]`

?

Last updated: Dec 20 2023 at 11:08 UTC