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时类型为Set的Bool

我当然想要做一些更复杂的事情(我知道上面的内容在几个方面是多余的),但关键是x \？= y不是Bool类型,它是Set类型,我不知道知道如何将该Set变成Bool.谢谢.

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!}

孔中的CC Cd给出了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有两个构造函数:yes和no,你可以在模式匹配中使用它们:

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

Relation.Nullary.Decidable模块中有一个函数,它将a 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 ?