Zulip Chat Archive

Stream: new members

Topic: noncomputable theory


Bryan Gin-ge Chen (Feb 08 2021 at 20:01):

I think I'm confused as to what noncomputable theory does. I thought that having noncomputable theory at the top of a file means that you don't have to add noncomputable explicitly anymore.

However, this commit implements a suggestion I made to remove noncomputable from a def in a file that starts with noncomputable theory and Lean complains.


Last updated: Dec 20 2023 at 11:08 UTC