伊德里斯1.2.0。我试图自动找到向量长度小于3的证明。
f : {n : Nat} -> {auto prf: n < 3 = True} -> Vect n a -> ()
f v = ()
f' : {n : Nat} -> {auto prf: isJust (natToFin n 3) = True} -> Vect n a -> ()
f' v = ()
这两种类型检查都可以使用f {n=2} [1, 2}，甚至可以使用，f (the (Vect 2 Nat) [1, 2])但是当我将其命名为时f [1, 2]，我得到
When checking argument x to constructor Data.Vect.:::
No such variable len
我还尝试了另一种方法：
g : {x : Fin 3} -> Vect (finToNat x) a -> ()
g v = ()
这也适用g {x=2} [1, 2]，但再次失败g [1, 2]
When checking an application of function Main.g:
Type mismatch between
Vect 2 Integer (Type of [1, 2])
and
Vect (finToNat x) Integer (Expected type)
Specifically:
Type mismatch between
2
and
finToNat x
好的，我猜这两个表达式在x未知时不会还原为相同的规范形式。
我不明白第一个错误。我怀疑它与[]语法重载有关。我究竟做错了什么？
当尝试解决统一问题时，Idris不会尝试逆转（内射）函数finToNat来猜测其值。因此，它只是卡住了。xfinToNat x = 2
在更一般的水平上，而不是将计算推入类型或在隐式参数中进行证明搜索，我将通过以下两种方法来表示有界向量：
record BoundedVec (n : Nat) (a : Type) where
size : Nat
less : LTE size n
vect : Vect size a
或者，遵循Agda的标准库
data BoundedVec : (n : Nat) -> (a : Type) -> Type where
Nil : BoundedVec n a
Cons : a -> BoundedVec n a -> BoundedVec (S n) a
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句