Stream: math-comp users

Topic: tval tcast


view this post on Zulip Florent Hivert (Aug 26 2021 at 16:28):

Maybe I'm rusty, but I've hard time finding the proof of this one. Do you think it is worth adding ?

Lemma tval_tcastE m n (eq_mn : m = n) (t : m.-tuple T) :
  tcast eq_mn t = t :> seq T.
Proof. by case: n / eq_mn. Qed.

view this post on Zulip Pierre Jouvelot (Aug 26 2021 at 19:21):

Florent Hivert said:

Maybe I'm rusty, but I've hard time finding the proof of this one. Do you think it is worth adding ?

Lemma tval_tcastE m n (eq_mn : m = n) (t : m.-tuple T) :
  tcast eq_mn t = t :> seq T.
Proof. by case: n / eq_mn. Qed.

I vote +1 for the proposal, since I needed it once and Emilio had to show me the proof, which was not obvious to me. It would be useful to beginners.


Last updated: Mar 29 2024 at 11:01 UTC