import for classical

Stream: new members

[Martin Dvořák]

What is the minimum import that will allow me to write noncomputable theory open_locale classical please?

[Kevin Buzzard]

noncomputable theory is in core Lean. For open_locale classical just find an occurrence of it in mathlib, import that file, type open_locale classical and then right click on classical to see where it takes you, and import that file instead.