Zulip Chat Archive

Stream: lean4

Topic: noncomputable theory

Horatiu Cheval (Mar 11 2022 at 19:04):

Is there a Lean 4 counterpart to noncomputable theory?

Gabriel Ebner (Mar 11 2022 at 19:05):

It's noncomputable section.

Horatiu Cheval (Mar 11 2022 at 19:14):

Thanks! That's even nicer than it was in 3, being able to modularizenoncomputable like this with sections :)

Gabriel Ebner (Mar 11 2022 at 19:22):

Oh wow, I've only noticed now that noncomputable section actually opens a section...

Last updated: May 02 2025 at 03:31 UTC