Zulip Chat Archive

Stream: new members

Topic: Casting Functions


view this post on Zulip 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)?

view this post on Zulip Eric Wieser (Jan 06 2021 at 18:26):

This works:

example (n n' : ) (h : n' = n) (f : fin n  ) : fin n'   := f  fin.cast h

view this post on Zulip 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.

view this post on Zulip 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