Zulip Chat Archive

Stream: new members

Topic: inferring coe as a function


view this post on Zulip Yakov Pechersky (Sep 08 2020 at 18:47):

Why is coe not inferred as a function in the second rw attempt below?

import data.fin

-- works
example {n : } (x : fin (n + 1)) (y : fin n) :
  ((x.succ_above y) : ) = (ite (y.cast_succ < x) (y : ) ((y : ) + 1)) :=
begin
  unfold fin.succ_above,
  rw apply_ite (coe),
  simp
end

-- rw fails
example {n : } (x : fin (n + 1)) (y : fin n) :
  ((x.succ_above y) : ) = (ite (y.cast_succ < x) (y : ) ((y : ) + 1)) :=
begin
  unfold fin.succ_above,
  rw apply_ite _ (y.cast_succ < x) y.cast_succ y.succ,
  sorry
end

view this post on Zulip Kenny Lau (Sep 08 2020 at 18:48):

function unification is noncomputable


Last updated: May 12 2021 at 04:19 UTC