时间戳

首页 > 解决方案 > 找出所有函数参数模式匹配

agda - 找出所有函数参数模式匹配

问题描述

有：

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

data One : Bin → Set where
  one : One (x1 nil)
  y0_ : ∀ {bin : Bin} → One bin → One (x0 bin)
  y1_ : ∀ {bin : Bin} → One bin → One (x1 bin)

one-ident : ∀ {x : Bin} → One x → to (from x) ≡ x

生成所有函数参数模式匹配的逻辑是什么？

one-ident one = {!   !}
one-ident {x0 x} (y0 o) = {!   !}
one-ident {x1 x} (y1 o) = {!   !}

例如，知道第一个参数是{x0 x}为什么第二个参数必须是(y0 o)？为什么第二个论点不能是(y1 o)？

代码示例取自此处。

标签： agda

解决方案

one-ident : ∀ {x : Bin} → One x → to (from x) ≡ x
one-ident one = {!   !}
one-ident {x0 xx} (y0 o) = {!   !}
one-ident {x1 xx} (y1 o) = {!   !}

当您知道它x是x0 xxone-ident 时，您就知道第二个参数的类型是One (x0 xx)。只有 1 个构造函数One可以具有该类型，即y0_.

推荐阅读