问电感级的Idris证明
EN

Stack Overflow用户

提问于 2017-10-06 08:13:16

回答 1查看 86关注 0票数 4

考虑以下功能

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)

试图编译时，我会得到以下错误：

When checking argument prf to Hanoi.tryMove:
        Type mismatch between
                So True (Type of Oh)
        and
                So (from /= to) (Expected type)

        Specifically:
                Type mismatch between
                        True
                and
                        not (Hanoi.Peg implementation of Prelude.Interfaces.Eq, method == from to)

关于tryMove的递归调用。如果我明确地传递给{prf}，如

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to {prf} (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to {prf} restOfTheDisposition)

它编译正确。

为什么Idris不能在归纳步骤中自动检测到证据，而能够在函数的正常调用中进行验证？

编辑：

下面是要使用的完整要点：https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

idris

回答 1

Stack Overflow用户

回答已采纳

发布于 2017-10-06 10:33:14

您提供了prf的默认值(prf)，因此Idris试图将Oh传递到递归调用中。Oh有So True类型，Idris希望prf为So (from /= to)类型，但是由于您不破坏to和from，Idris无法知道from /= to的值，这就是您看到错误消息的原因。

您可以将签名更改为包含{auto prf: So (from /= to)}或完全删除prf参数，因为您实际上并不使用它，只需将其传递到递归调用中，而无需任何修改。

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/46601247

复制

相似问题

问电感级的Idris证明
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问电感级的Idris证明EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问电感级的Idris证明
EN