代码之家 › 专栏 › 技术社区 › simpadjo

Idris:模式匹配后重建相等

dependent-type idris

0

simpadjo · 技术社区 · 6 年前

我正在将一个列表分解为头尾两部分,但稍后我需要一个证明,证明它们在合并时还给了我原始列表:

test: Bool -> String
test b = let lst = the (List Nat) ?getListFromOtherFunction in
        case lst of
          Nil => ""
          x :: xs =>
            let eq = the ((x::xs) = lst) ?howToDoIt in ""

我用的是IDRIS1.3.1。

1 回复 | 直到 6 年前

1

2

Alexander Gryzlov 6 年前

您可以使用依赖模式匹配:

test: List Nat -> String
test lst with (lst) proof prf
  | Nil = ""
  | (x :: xs) = ?something

在这里 prf 会保持你的平等。

lst 在LHS中,您的证明将在需要时自动简化。

推荐文章

lodo · 依赖类型:在归纳类型中强制全局属性

7 年前

Rastislav Kassak · 为什么Idris中的Nat数据类型以0开头而不是1?

8 年前

maiermic · 如何确定HVect的所有子维度?

8 年前

Aadit M Shah · 如何使用Agda中N的归纳原理证明N的递归器的定义方程命题成立?

9 年前

J. Abrahamson · 异构列表中的单体

9 年前