-
чет туплю, есть
as :: V a n
bs :: V a n1
ev :: n ~ n1
f :: V a n -> V a n -> V a n
как применить f as (_wtf bs)?
я так понимаю, мне нужно имея ev, доказать что V a n :~: V a n1?
Replies (19)
-
-
@PineappleZombie, пасиб, у меня уже тоже, нужно или sym или n1 и n в типе поменять местами
-
@PineappleZombie, data SV a = forall n . KnownNat n => SV (V a n)
-
@PineappleZombie, с UniNaturals поидее все просто, а тут гад не хочет выводить, что если n — KnownNat, то n+1 — тоже KnownNat.
-
@qnikst, Да, индукции тут нема, можно либо сконвертировать длину списка в SomeNat someNatVal, и сделать V a n при поможи небезопасной функции, ну или сконвертировать Nat в число Пеано (костыльно страшно)
-
@PineappleZombie, вот похоже, что да или unsafeCoerce или Пеано.. жуть.
-
@qnikst, Впрочем пугающий изоморфизм между Пеано и Nat у меня есть готовый
-
@PineappleZombie, ну мне это пока на поиграться было, так что возможно есть смысл самому сделать
