extends

Stream: new members

[Bjørn Kjos-Hanssen]

Is there a way to avoid having to write .to_mwe here? I feel like it should be obvious that we want .to_mwe so we shouldn't have to say it.

structure mwe :=
mk :: (f:ℕ→ℕ)
lemma mwe_lemma (x : mwe): x.f = x.f := rfl -- imagine the proof was very long
structure mwe' extends mwe :=
mk :: (g:ℕ→ℕ)
lemma mwe_lemma' (x: mwe'): x.f = x.f := mwe_lemma x.to_mwe

[Eric Rodriguez]

in these cases we usually write to_mwe as an instance of docs#has_coe, see for example docs#units.has_coe

[Bjørn Kjos-Hanssen]

Thanks @Eric Rodriguez . Following your answer I got this to work:

instance my_coe : has_coe mwe' mwe:=
{coe := λ M: mwe', M.to_mwe}

lemma mwe_lemma' (x: mwe'): x.f = x.f := mwe_lemma x