Stream: new members
Topic: Casting Functions
Marcus Rossel (Jan 06 2021 at 18:22):
Let's say I have
(n n' : ℕ) (h : n' = n) (f : fin n → ℤ).
What's the nicest way to get
f' : fin n' → ℤ from this (where
∀ x, f x = f' x)?
Eric Wieser (Jan 06 2021 at 18:26):
example (n n' : ℕ) (h : n' = n) (f : fin n → ℤ) : fin n' → ℤ := f ∘ fin.cast h
Kevin Buzzard (Jan 06 2021 at 18:43):
This is a great example of dependent type hell. It seems that in dependent type theory one has to learn to think about these questions in a certain kind of way in order to avoid pain.
Marcus Rossel (Jan 06 2021 at 19:02):
@Kevin Buzzard ^^ indeed. This is part of an effort to get out of dependent type hell.
Last updated: May 13 2021 at 05:21 UTC