noncomputable instances

Stream: mathlib4

[Jihoon Hyun]

There are some noncomputable instances (defs?) which are actually computable, one of them being docs#Function.Embedding.fintype. The doc says working with computable instances were some sort of a pain, but I'm not sure why. How would it affect Mathlib if such instances were computable? Is appending noncomputable keyword to computable objects really worth it?

[Michael Rothgang]

If you can remove the noncomputable keyword (while the proof still compiles) and the file doesn't become slower, usually a PR doing so is fine.

[Michael Rothgang]

(This keyword could be there for historical reasons: either Lean's noncomputable check being more strict, or compilation of definitions taking a long time. Both have improved significantly in the past year or two.)

[Aaron Liu]

I had a PR making it computable but it also did a bunch of other stuff

[Aaron Liu]

#22919