## Stream: general

### Topic: cast

#### Kenny Lau (Jun 10 2019 at 15:23):

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 (Jun 10 2019 at 15:23):

I feel like cast isn't used enough

#### Kenny Lau (Jun 10 2019 at 15:23):

here's a theorem I proved with cast

#### Mario Carneiro (Jun 10 2019 at 15:25):

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

#### Mario Carneiro (Jun 10 2019 at 15:25):

it's also not much different from eq.rec

#### Wojciech Nawrocki (Jun 11 2019 at 16:55):

@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 (Jun 11 2019 at 20:10):

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

Last updated: Dec 20 2023 at 11:08 UTC