Для чего предназначена каждая из этих программ и что они предлагают друг другу? Кроме того, согласованы ли обе системы и, более того, основаны ли они на какой-то фундаментальной математической теории? Меня волнуют две вещи: Легко установить...

Я хотел доказать, что if there is m which is less than 10 and there is n which is less than 15 then there exist z which is less than 25. thm : ((∃ λ m → (m < 10)) AND (∃ λ n → (n < 15))) -> (∃ λ z → (z < 25)) thm = ? Как...

Я хочу доказать, что существует натуральное число меньше 10. Я пишу код таким образом .. thm2 : (∃ λ m → (m < 10)) thm2 = zero , s≤s z≤n Я не могу понять, как это работает. Пожалуйста, объясни..

Я определил Поток положительного рационального следующим образом. one : ℤ one = + 1 --giving a rational as input it will return next rational (in some down tailing method) next : pair → pair next q = if (n eq one) then (mkPair (+ m Data.Integer.+...

Это min определение ниже работает с двумя церковными числами и возвращает наименьшее значение. Каждое число становится продолжением, которое отправляет свое предысторию другому, зигзагообразно и загадочно, до тех пор, пока не будет достигнут ноль....

Я хотел бы автоматически регистрировать аргументы, используя синтаксис, объявленный помимо синтаксиса, указанного в качестве конструктора типа. Например, postulate P : ℕ → ℕ → Set data Silly : Set where goo : (n : ℕ) → Fin n → (m : ℕ) → Fin m...

Я, вероятно, не буду подходить к этому наилучшим образом, поскольку Agda и, в частности, стандартная библиотека Agda все еще для меня в новинку. Я пытаюсь реализовать понятие двоичных деревьев поиска. У меня есть простое определение двоичного...

Учитывая следующий тип данных, который кодирует проверенное сравнение двух натуральных чисел: open import Agda.Builtin.Nat data Compare : Nat -> Nat -> Set where LT : {m : Nat} {n : Nat} -> Compare m (suc (m + n)) EQ : {m : Nat}...

Я новичок в языке Agda, и я работаю над формальными языками, используя Agda. У меня возникают проблемы с доказательством ассоциативности конкатенации языков. Доказательство будет выделено желтым цветом, поскольку Agda не смогла найти слова для "++...

Я использую готовую версию Windows Agda 2.4.2.2. В Emacs / Agda2 Include Dirs я определил c: /agda-stdlib-0.13/src и папки на один уровень ниже. При загрузке модуля, состоящего только из этих двух строк, я получаю сообщение об ошибке. module...

Это кажется невозможным для извлечения второго элемента сигмы по исчислению конструкций. Более того, похоже, что не существует известного простого способа расширить исчисление конструкций с зависимыми исключениями без потери согласованности. Таким...

TL; DR: в Agda, учитывая a : A и proof : A == B , могу ли я получить элемент a : B ? В моей постоянной попытке изучить Agda я создал следующий Prime : nat -> Set тип данных, который свидетельствует о примитивности естественного....

Как в Agda правильно закодировать набор; то есть список уникальных элементов? Что я пробовал: Это можно сделать, используя один из предложенных методов на моем последний вопрос , заключающийся в том, чтобы закодировать предикат is-set как...

В Agda 2.6.0.1 я хотел бы использовать нерелевантный термин доказательства в записи, а затем показать, что две из этих записей равны только на основе их терминов данных. data Bools : Set where T : Bools F : Bools record Thing : Set where...

Я только начал изучать Agda, читая Основы языка программирования в Agda . Прямо в первой главе есть определение умножения, причем один из случаев — (suc m) * n = n + (m * n) . Я предположил, что это может быть лучше выражено как (m + 1) * n = n +...