Есть ли способ добавить все леммы в базу данных подсказок в ядро, чтобы мне не приходилось писать auto with foo везде в файле?
Объединение баз данных подсказок в ядро
comment
почему бы вам не определить собственную тактику на этот случай?
- person ejgallego schedule 06.12.2019
Ответы (1)
Пока вам не нужно чередовать леммы из разных баз данных, вы можете написать
Hint Resolve 1 => solve [ auto with foo ] : core.
person
Jason Gross
schedule
06.12.2019
Не тихо то, что я искал, но я возьму то, что получу.
- person Ifaz Kabir; 07.12.2019
Действительно, то, что вы хотите, в настоящее время невозможно без написания собственного плагина. Однако существует существующий запрос функции, которую вы хотите: github.com/ coq/coq/issues/7650#issuecomment-459966243
- person Jason Gross; 07.12.2019
