Вопросы с тегом Кок

0 голосов

1 ответ

типы как параметры в coq

push33n / 12 марта 2020

0 голосов

0 ответов

SSreflect не работает с Emacs, Coq и ProofGeneral. Как установить SSreflect в MacOS?

Vedant Chavda / 11 марта 2020

0 голосов

1 ответ

Конструктор Coq не может принимать два аргумента разных типов?

push33n / 11 марта 2020

0 голосов

0 ответов

Как манипулировать неравенствами и равенствами в Coq?

Iva Kam / 11 марта 2020

0 голосов

1 ответ

Generi c равенство подъема в к

Iva Kam / 10 марта 2020

0 голосов

1 ответ

Как доказать неравенство членов, порожденных двумя разными конструкторами одной и той же индуктивности в coq?

Iva Kam / 10 марта 2020

0 голосов

1 ответ

(A -> B) / \ (B -> C) -> (A -> C) в Coq?

Kaind / 09 марта 2020

1 голос

1 ответ

Как мне описать умножение векторизованных матриц?

Kazunari Tanaka / 07 марта 2020

0 голосов

1 ответ

Основы Coq

Javier / 06 марта 2020

0 голосов

1 ответ

Coq использовать уточнение с двойным подтекстом

mdatsev / 04 марта 2020

0 голосов

1 ответ

Coqtop не может загрузить файл

yuanqili / 04 марта 2020

0 голосов

1 ответ

Положение элементов в списке

laiba naz / 03 марта 2020

0 голосов

1 ответ

coq c: -Q.PLF: нет такого файла или каталога

Curious Person / 02 марта 2020

1 голос

1 ответ

COQ Proof Assistant - Примените гипотезу

Rodny / 28 февраля 2020

1 голос

1 ответ

Невозможно доказать, что только 0 меньше 1 с помощью finTypes mathcomp

jabberabbe / 27 февраля 2020

0 голосов

1 ответ

Как сделать тип с конечным множеством, используя MSets с «обычным» равенством?

pipsqueaker117 / 26 февраля 2020

1 голос

1 ответ

Трудности Coq в определении конструкторов с использованием принудительных типов

pipsqueaker117 / 25 февраля 2020

2 голосов

1 ответ

Доказательство общей ассоциативности в группах

Callum MacAskill / 20 февраля 2020

0 голосов

3 ответов

Как доказать равенство из равенства некоторых

he11boy / 19 февраля 2020

0 голосов

1 ответ

Выражение «почти правильность» под опцией типа

zoickx / 18 февраля 2020

0 голосов

0 ответов

Почему Proof General так медленно работает в Windows 10?

Javier / 17 февраля 2020

0 голосов

1 ответ

Могу ли я использовать функции в Coq в качестве конструкторов?

Someone / 16 февраля 2020

0 голосов

1 ответ

Почему удаление предположений меняет поведение индуктивных тактов c?

Carl Patenaude Poulin / 13 февраля 2020

0 голосов

1 ответ

Теорема о вставке в BST в coq

Marco Mantovani / 10 февраля 2020

0 голосов

1 ответ

Можно ли превратить шаблон контекста в функцию Галлина?

dunnl / 09 февраля 2020