Importing analysis.normed_spaced makes things noncomputable

Stream: new members

[Abhimanyu Pallavi Sudhir]

The following code:

import data.real.basic

def seq : Type := ℕ → ℝ
def seq_add : seq → seq → seq := λ s t n, s n + t n

Works perfectly fine, but if I add import analysis.normed_spaceto the top, seq_add becomes noncomputable, it depends on real.normed_field. But this line works perfectly with or without the import:

def seq_smul (c : ℝ) : seq → seq := λ s n, c * (s n)

[Mario Carneiro]

hm, I guess the instance priorities need adjustment