Idris ：是否可以使用 "with" 重写所有函数以使用 "case" 而不是 "with" ？如果不是，你能举个反例吗？

Question

在 Idris 中，是否可以重写所有使用“with”的函数以使用 "case" 而不是 "with"？

如果不是，能举个反例吗？

Answer 1

不可能。当您使用 with 进行模式匹配时，上下文中的类型将使用从匹配的构造函数中提取的信息进行更新。 case 不会导致此类更新。

例如，以下适用于 with 但不适用于 case：

import Data.So

-- here (n == 10) in the goal type is rewritten to True or False
-- after the match
maybeTen : (n : Nat) -> Maybe (So (n == 10))
maybeTen n with (n == 10)
  maybeTen n | False = Nothing
  maybeTen n | True  = Just Oh

-- Here the context knows nothing about the result of (n == 10)
-- after the "case" match, so we can't fill in the rhs
maybeTen' : (n : Nat) -> Maybe (So (n == 10))
maybeTen' n = case (n == 10) of
  True  => ?a 
  False => ?b

Idris ：是否可以使用 "with" 重写所有函数以使用 "case" 而不是 "with" ？如果不是，你能举个反例吗？

Idris : Is it possible to rewrite all functions using "with" to use "case" instead of "with" ? If not, could you give a counter example?

idris