Я новичок в 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, и был бы признателен, если бы кто-нибудь мог направить меня к руководствам или примерам, использующим его для доказательства логических утверждений.
