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

2 голосов

1 ответ

Как в coq использовать лемму a = b в обратном порядке?

mercury0114 / 16 июня 2020

0 голосов

0 ответов

Установка библиотеки для Coq через Opam на Windows

Alex Mal / 05 мая 2020

0 голосов

1 ответ

Докажите свойства списков относительно содержания

Attila Karoly / 04 мая 2020

1 голос

1 ответ

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

Warrick Macmillan / 04 мая 2020

1 голос

1 ответ

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

Warrick Macmillan / 02 мая 2020

1 голос

1 ответ

compatibility.vo содержит библиотеку Top.comparable, а не библиотеку, сопоставимую

Ayman Osman / 02 мая 2020

1 голос

1 ответ

Распределение вычитания над бигопом

Pierre Jouvelot / 02 мая 2020

2 голосов

2 ответов

Как доказать (2 ^ 2)% R = 4% R

kimitsu / 01 мая 2020

0 голосов

0 ответов

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

rosi javi / 30 апреля 2020

1 голос

1 ответ

Почему «Омега» Такти c не может решить такую простую проблему, как эта

yrZhang / 28 апреля 2020

3 голосов

1 ответ

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

Joald / 27 апреля 2020

3 голосов

1 ответ

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

yrZhang / 27 апреля 2020

2 голосов

2 ответов

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

Warrick Macmillan / 27 апреля 2020

1 голос

1 ответ

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

Warrick Macmillan / 26 апреля 2020

1 голос

0 ответов

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

Ahsim Nreiziev / 23 апреля 2020

2 голосов

1 ответ

Unicode символы не для Proof-general при написании Coq

Javier / 23 апреля 2020

3 голосов

1 ответ

Как изменить версию Coq в Proof General?

Isaac Velasquez / 22 апреля 2020

2 голосов

1 ответ

Ошибка VST forward_call при нестандартном соглашении о вызовах

Yarick / 21 апреля 2020

3 голосов

1 ответ

В чем разница между Аксиомой и Переменной в Coq

radrow / 21 апреля 2020

3 голосов

1 ответ

Классические аксиомы подразумевают, что каждое предложение разрешимо?

Sven Williamson / 20 апреля 2020

2 голосов

1 ответ

Невозможно настроить сертифицированное программирование с зависимыми типами

Javier / 19 апреля 2020

3 голосов

1 ответ

Тип неравенства без аргументов кардинальности

Isaac van Bakel / 18 апреля 2020

2 голосов

1 ответ

Как доказать отсортированный список

laiba naz / 18 апреля 2020

1 голос

1 ответ

Приведите пример в Coq, где (AB: Prop), P: Prop -> Type, такой, что A <-> B, но нельзя заменить PA на PB

Siddharth Bhat / 16 апреля 2020

1 голос

1 ответ

Доказать, что два жителя в Проп не равны?

Siddharth Bhat / 16 апреля 2020