从 case 语句证明两个值相等

【问题标题】：Prove two values are equal from case statement从 case 语句证明两个值相等
【发布时间】：2017-11-07 01:18:06
【问题描述】：

以下示例使用来自Bi package 的Data.Bin：

import Data.Bin

foo : (x, y : Bin) -> Dec (binCompare x y = LT)
foo x y = case binCompare x y of
    LT => Yes (C1 ?hole1)
    EQ => ...
    GT => ...

:t ?hole1
binCompare x y = LT

在处理LT 案件时，如何获得binCompare x y = LT 的证据？

【问题讨论】：

标签： pattern-matching typechecking idris unification

【解决方案1】：

您需要使用view 而不是case：

由于类型可以依赖于值，因此某些参数的形式可以由其他参数的值决定。

所以下面的版本按预期工作：

foo : (x, y : Bin) -> Dec (binCompare x y = LT)
foo x y with (binCompare x y)
  foo x y | LT = Yes Refl
  foo x y | EQ = ?q_2
  foo x y | GT = ?q_3

【讨论】：