本文介绍了删除元组的tcast的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
我陷入了这样的目标平等的困境(我认为细节无关紧要):
I'm in a bind with a goal equality like this (the details don't matter, I think):
tcast tc0
[tuple of take i (s_bs bs) ++ drop i.+1 (s_bs bs) ++ [:: [ffun⇒ 0]]]
=
...
如何摆脱 tcast 和 tuple 回到简单的 seq (我尝试了 val_inj 技巧，但这似乎并没有删除类型转换)?
How do I get rid of the tcast and tuple to go back to simple seq (I tried the val_inj trick, but this didn't seem to remove the type cast)?
谢谢.
再见
皮埃尔
推荐答案
给出准确的答案有些困难，因为您没有提供任何可重现的测试用例.但是，一旦您应用了 val_inj ，就可以尝试使用以下引理重写目标.
Giving a precise answer is a bit difficult, since you did not provide any reproducible testcase. But you could try rewriting your goal using the following lemma, once you have applied val_inj.
Lemma val_tcast {T} m n (tc : n = m) (x : n.-tuple T) :
val (tcast tc x) = val x.
Proof. now case tc. Qed.
这篇关于删除元组的tcast的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！