我是 Agda 新手，需要帮助来理解 Decidable 函数和 Dec 类型。
我正在尝试定义一个一阶逻辑谓词，并且我想用某种 bool 值的证明进行编码。我发现执行此操作的方法是使用 Dec 类型..
现在，据我所知，为了能够做到这一点，我必须将所有逻辑运算符重新定义为可判定类型而不是集合类型。为此，我将其嵌入到新类型中，这就是我对 and 运算符所做的操作:
data _∧_ (A B : Set) : Set where
_&_ : A → B → A ∧ B
Dec∧ : {A B : Set} → A ∧ B → Dec (A ∧ B)
Dec∧ A∧B = yes (A∧B)
这是可行的方法，还是有其他方法？
然后，我想使用这个运算符来定义 Nat 值的关系，所以我做了这样的事情:
_◆_ : ℕ → ℕ → Dec∧ (Rel ℕ lzero) (ℕ → Set)
x ◆ y = (0 < x) ∧ (x ² ≡ 2 * y ²)
但这会产生类型错误..
我不确定如何使用 Dec，如果有人能指导我使用它来证明逻辑陈述的教程或示例，我将不胜感激。
最佳答案
基本上，可判定谓词是这样的谓词，我们有一个算法，该算法在有限时间内终止，并返回"is"以及其为真的证明，或者返回“否”及其否定证明。例如，对于每两个自然数，我们可以证明它们相等或不相等。
您所写的内容不会进行类型检查。你的函数应该返回 Dec (Rel ℕ lzero) (ℕ → Set)，第一个参数是正确的，但第二个参数不是。它应该是一个函数，例如\x -> 2 * x。
附注对我来说这个函数没有任何意义。您想用它实现什么目标？
关于agda - Agda 中的可判定谓词，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22367762/