我是 Agda 的新手，我需要帮助来了解Decidable功能和Dec类型。
我正在尝试定义一阶逻辑谓词，并且我想用证明对某种布尔值进行编码。我发现这样做的方法是使用 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，如果有人可以指导我使用它来证明逻辑陈述的教程或示例，我将不胜感激。