Вопросы с тегом кок-tacti-c

1 голос

1 ответ

Изменение, работа и применение выражений let в Coq

Warrick Macmillan / 04 мая 2020

1 голос

1 ответ

Применяя зависимый тип к аргументу, чтобы утверждать цель в Coq?

Warrick Macmillan / 02 мая 2020

2 голосов

2 ответов

Как определить пользовательский принцип индукции в coq?

Warrick Macmillan / 27 апреля 2020

1 голос

1 ответ

Как явно использовать принцип индукции в coq?

Warrick Macmillan / 26 апреля 2020

1 голос

0 ответов

Доказательство от противоречия в Coq (НЕ Elimtype False)

Ahsim Nreiziev / 23 апреля 2020

0 голосов

1 ответ

Вариант индуктивной тактики c, который не требует использования `запомнить` на подтермах

Carl Patenaude Poulin / 09 апреля 2020

1 голос

1 ответ

Показать, что термин не равен строго большему

Carl Patenaude Poulin / 09 апреля 2020

2 голосов

1 ответ

Как использовать решающую тактику Coq arithmeti c с арифметикой SSReflect c

LogicChains / 04 апреля 2020

1 голос

3 ответов

Докажите равенство в списке, построенном с помощью карты

Carl Patenaude Poulin / 25 марта 2020

2 голосов

1 ответ

Как мне упростить гипотезу вида True -> P в Coq?

psquid / 23 марта 2020

1 голос

1 ответ

Автоматически специализировать поля, когда параметры находятся в области видимости

Carl Patenaude Poulin / 18 марта 2020

0 голосов

1 ответ

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

Kaind / 09 марта 2020

0 голосов

1 ответ

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

mdatsev / 04 марта 2020

1 голос

1 ответ

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

Rodny / 28 февраля 2020

0 голосов

3 ответов

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

he11boy / 19 февраля 2020

0 голосов

1 ответ

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

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

1 голос

2 ответов

Различить цель в Coq

he11boy / 08 февраля 2020

0 голосов

1 ответ

Рассуждения с сопоставлениями с образцами в Coq

Nicolás / 08 февраля 2020

0 голосов

2 ответов

Как уничтожить список в Coq (ноль или нет ноль)

he11boy / 06 февраля 2020

0 голосов

1 ответ

Как показать инъективность функции?

Max Heiber / 11 января 2020

0 голосов

1 ответ

Как я могу закрыть эту демонстрацию о opt_ c в coq?

Marco Mantovani / 05 января 2020

Для получения более полной информации посмотрите в списке вопросов или в популярных тегах.

...