agda - "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 -陈述和没有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用途 y由 inj₂ y 决定

实际的构造函数名称来自 ⊎ 的定义- 查看something-even的类型连接类型 Even n和 Even (suc n) .所以x在 inj₁ x对应于 Even n 类型的值给定 n , 和 y在 inj₂ y对应于 Even (suc n) 类型的值对于相同的 n .