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