agda - Agda 中的平等测试分支？ (基本的)

一个非常基本的问题，但作为 Agda 初学者，我很难过。

我只想检查两个术语是否相等并根据不同的情况返回不同的东西。我可以编写自己的相等测试器，但是我如何使用 equiv(或者正确的方法是什么)来做到这一点？

这是一个最小的例子:

import Data.Nat
import Relation.Binary
myeqtest : ℕ → ℕ → ℕ
myeqtest x y = if x Data.Nat.≟ y then true else false

错误信息:
.Relation.Nullary.Core.Dec (x .Relation.Binary.Core.Dummy.≡ y) !=<
集合类型的 bool 值
当检查表达式 x Data.Nat.≟ y 的类型为 Bool 时

我当然想做一些更复杂的事情(我知道上面在几个方面是多余的)，但重点是 x\?= y 不是 Bool 类型，它是 Set 类型，而我没有知道如何将 Set 变成 Bool。谢谢。

最佳答案

无聊的进口:

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.Core
open import Data.Bool hiding (_≟_)
open import Data.Nat

现在让我们问问 Agda ，她是怎么想的:

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y = {!x ≟ y!}

孔中的 C-C C-d 给出 Dec (x ≡ y) 。 Dec 是关于可判定命题的，在 Relation.Nullary.Core 模块中定义:

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

IE。总是存在 P 或 ¬ P 的证明，其中 ¬ 的意思是“不是”。对于某些命题，这只是一个手工制作的排中律。在我们的例子中，总是存在一个证明，即一个数字等于或不等于另一个。

所以 Dec 有两个构造函数: yes 和 no ，你可以在模式匹配中使用它们:

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y with x ≟ y
... | yes _ = true
... | no  _ = false

Relation.Nullary.Decidable 模块中有一个函数，可以将 Dec 转换为 Bool :

⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false

所以你可以将 myeqtest 定义为

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y = if ⌊ x ≟ y ⌋ then true else false

或者干脆

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y = ⌊ x ≟ y ⌋

关于agda - Agda 中的平等测试分支？ (基本的)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/27306619/