“with”关键字在 agda 中如何工作？还有下面的代码？？

Question

我无法清楚地理解它。我试图学习“with”关键字，但我也有疑问。请帮忙 ！！！

我想了解“with”的工作原理和这段代码的工作原理。

something-even : ∀ n → Even n ⊎ Even (suc n)
something-even zero = inj₁ zero
something-even (suc n) with something-even n
... | inj₁ x = inj₂ (suc-suc x)
... | inj₂ y = inj₁ y
(this states that either n is even or its successor is even). In fact, thm0 can be implemented without using recursion!

thm0 : ∀ x → ∃ λ y → Even y × x less-than y
thm0 n with something-even n
... | inj₁ x = suc (suc n) , suc-suc x , suc ref
... | inj₂ y = suc n , y , ref

Answer 1

如果您熟悉 Haskell，您会注意到在 Agda 中没有 if-statements 和 case。

with 对表达式结果进行模式匹配。例如，with something-even n 计算 something-even n，然后在以下行中与 ... | inj₁ x 和 ... | inj₂ y 进行模式匹配。这些匹配表达式，查看其值是使用inj₁ 还是inj₂ 构造函数构造的，以便它们包装的值可以在右侧表达式中使用：suc (suc n) , suc-suc x , suc ref 使用x 确定inj₁ x 和 suc n , y , ref 使用由 inj₂ y 确定的 y

实际的构造函数名称来自⊎ 的定义——参见something-even 的类型连接类型Even n 和Even (suc n)。因此，inj₁ x 中的x 对应于给定n 的Even n 类型的值，inj₂ y 中的y 对应于相同Even (suc n) 的Even (suc n) 类型的值。