Implicitly coerce Fin n to Fin m, where n

Stream: general

---

[Konstantin Weitz]

I'm struggling to implement this, since Coe seems to require all implicit parameters to be deliverable from the source type

[Yakov Pechersky]

Coercion here is working through the typeclass synthesis system. That system needs access to all facts to synthesize. On the fly, it can't prove n < m and use that for its synthesis, unless you have an explicit [Fact (n < m)] for your specific n and m available.

[Yakov Pechersky]

Do you really need implicit coercion, or could you do an at-site-of-call lift? Via CanLift and the lift tactic.

[Robin Arnez]

Something like

class Decide (p : Prop) [Decidable p] where
  out (p) : p

instance : @Decide p (Decidable.isTrue h) := @Decide.mk _ (_) h

local instance [Decide (n ≤ m)] : CoeDep (Fin n) x (Fin m) := ⟨x.castLE (Decide.out (n ≤ m))⟩

variable (x : Fin 3)
#check (x : Fin 5)

should work

[Violeta Hernández]

Or you know, you could simply do the coercion explicitly as ⟨x.1, by decide⟩