在 Idris 中,是否可以使用“重写所有函数”with” 使用“case”而不是“with”?
如果不是,能举个反例吗?
不可能。当你模式匹配时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
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)