noncomp_error.lean:1:0: error: definition 'a' was incorrectly marked as noncomputable