noncomputable definition a := 2
