cast

Stream: general

[Kenny Lau]

theorem cast_eq_of_heq : ∀ {α β : Sort u} {a : α} {b : β} (H : a == b), cast (type_eq_of_heq H) a = b
| α _ a _ heq.rfl := rfl

[Kenny Lau]

I feel like cast isn't used enough

[Kenny Lau]

here's a theorem I proved with cast

[Mario Carneiro]

cast is used exactly as often as it should be, which is almost never

[Mario Carneiro]

it's also not much different from eq.rec

[Wojciech Nawrocki]

@Mario Carneiro I run into casts all the time, but I would like to not use them, in accordance with your "almost never". However, I don't see any way to do that. For example, as soon as I define a few simple things, casts seem to become necessary really quickly:

variable vector: ℕ → Type
variable mk_vec: Π n: ℕ, vector n
variable consume_vec: Π x y, vector (x+y) → ℕ

-- Of course, I could just swap the x,y arguments to consume_vec here but this
-- doesn't seem to be possible very often with more complicated types.
def something_useful := λ x y, consume_vec x y $ cast (by simp) (mk_vec (y + x))

-- At what point does this go wrong? To me, it seems like
-- it goes wrong as soon as `vector` is defined the way it is here.

[Mario Carneiro]

you are right... it goes wrong as soon as you state the problem like that