在Agda的平等測試分支？ （基本）

Question

一個非常基本的問題，但作爲一個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）= < 類型的布爾設置 當檢查表達式xData.Nat.≟y具有類型Bool

我當然想要做更復雜的事情（我知道上述是多餘的），但重點是x \？= y不是Bool類型，它是Set類型的，我不知道如何將該Set設置爲一個布爾。謝謝。

Answer 1

鏜進口：

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

現在讓我們來問阿格達，她認爲：

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 

即總是存在P或¬ P的證明，其中¬表示「不」。對於某些命題，這僅僅是排除中等的手工定律。在我們的情況下，總是存在一個證明，即一個數字與另一個數字相等或不相等。

所以Dec有兩個contructors：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 ⌋