noncomputable theory

Stream: new members

[Bryan Gin-ge Chen]

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.