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