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

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

0 голосов
0 ответов

В моем проекте я пытаюсь добавить больше доказательств в определения функций, что неизбежно...

Jason Hu / 11 сентября 2018
0 голосов
1 ответ

Я пытаюсь реализовать зависимый тип оценщика STLC в Coq, используя Program Fixpoint.Поскольку в...

Jason Hu / 10 сентября 2018
0 голосов
1 ответ

Файл Coq Standard Library Coq.Init.Logic, который можно найти здесь , содержит оператор Notation...

Stefan / 09 сентября 2018
0 голосов
2 ответов

Я застрял с теоремой, которую легко сформулировать: «Если максимальный элемент вектора равен 0, то...

ged / 09 сентября 2018
0 голосов
1 ответ

Подумайте о функции, которая принимает Set и возвращает длину в байтах с именем byteLength:...

luochen1990 / 08 сентября 2018
0 голосов
1 ответ

Я доказываю простое математическое свойство для подмножеств, например: A подмножество B; о том, что...

Tom And. / 06 сентября 2018
0 голосов
0 ответов

Я пытаюсь перенести тактику Coq (в настоящее время написанную на Ltac) на OCaml, чтобы иметь...

ErikMD / 04 сентября 2018
0 голосов
0 ответов

Я пытаюсь смоделировать некоторые конкретные наборы (Ensembles) элементов, которые сами являются...

larsr / 04 сентября 2018
0 голосов
0 ответов

DropDownViewResource применяется к Spinner, но не к AutoCompleteTextView. Это работает:...

Denis / 04 сентября 2018
0 голосов
1 ответ

Согласно Теории гомотопического типа (стр. 49), это принцип полной индукции для равенства:...

V. Semeria / 02 сентября 2018
0 голосов
1 ответ

Для любых A B : Prop, sum A B и sumbool A B изоморфны, следующим образом, Definition from_sumbool...

V. Semeria / 01 сентября 2018
0 голосов
2 ответов

У меня есть ситуация, когда я определил индуктивный тип данных t и частичный порядок le над ним (ср

authchir / 31 августа 2018
0 голосов
1 ответ

В логических фондах Фондов программного обеспечения они используют идею индукции, чтобы доказать...

Innovative Inventor / 30 августа 2018
0 голосов
1 ответ

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

geppettodivacin / 30 августа 2018
0 голосов
1 ответ

Учитывая эти два типа, Inductive unit : Set := tt. Inductive otherUnit : Set := ttt. Может ли Coq...

V. Semeria / 30 августа 2018
0 голосов
1 ответ

В настоящее время я начал работать над доказательством теорем о логике первого порядка в Coq (...

ged / 30 августа 2018
0 голосов
1 ответ

Можем ли мы назначить кардиналов в Coq Prop, Set и каждому Type_i? Я вижу только определение...

V. Semeria / 28 августа 2018
0 голосов
2 ответов

Предположим, у меня есть некоторый язык программирования с отношением "имеет тип" и отношением...

jmite / 27 августа 2018
0 голосов
1 ответ

Я играю с индуктивными предложениями. У меня есть следующее индуктивное определение: Inductive...

Ilya Vlasov / 25 августа 2018
0 голосов
1 ответ

Я хотел бы создать зависимую функцию, но я сталкиваюсь с ошибкой несоответствия типов в термине...

geppettodivacin / 24 августа 2018
0 голосов
1 ответ

Этот вопрос основан на моем вопросе https://cs.stackexchange

TomR / 24 августа 2018
0 голосов
1 ответ

Я хотел бы реализовать в Coq что-то вроде следующего кода: Inductive IT := | c1 : IT | c2 (x:IT)...

ged / 24 августа 2018
0 голосов
0 ответов

Я недавно установил coq в своей системе (сначала из пользовательского репозитория arch, но затем...

John Dorian / 06 июля 2018
0 голосов
0 ответов

Я работаю из этой книги http://www.seas.upenn.edu/~cis500/current/sf/lf-current/, которая...

Adam / 04 июля 2018
0 голосов
1 ответ

В настоящее время я работаю над доказательствами, где снова и снова пишу такой код: Lemma eq_T:...

jmite / 04 июля 2018
Добро пожаловать на сайт PullRequest, где вы можете задавать вопросы и получать ответы от других членов сообщества.
...