证明两个值与case语句相等

Question

以下示例使用Data.Bin来自Bi包:

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

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

Answer 1

您需要使用视图而不是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