小编red*_*h64的帖子

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出:

其次,到目前为止,目前的实施工作进展有限,因此可能仍然存在一种情况,即它认为功能是总的而不是.不要依赖它来证明你的证明!

这是否意味着不能依赖Idris作为证据,或者是否有办法创建不需要整体检查的证明？

我已经在几种情况下运行,我想对一个带有可选功能的对象进行一系列操作." - >"适用于同一对象上的命令序列(例如(c(b(ax)))变为( - > xabc)),除非某些操作是可选的.例如,假设我想这样做:

(c
  (if (> (a x) 2)
     (b (a x))
     (a x)
     )
  )

有没有办法以更清晰的方式使用" - >"这样的操作？

为什么不会出现以下类型的问题:

v1 : mod 3 2 = 1
v1 = Refl

然而,这将很好地检查:

v2 : 3 - 2 = 1
v2 = Refl

以下是教程中的示例,为简单起见稍作修改:

data Vect : Nat -> (b:Type) -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

data Elem : a -> Vect n a -> Type where
  Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
  There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 …