Дело Идриса / тактика индукции

Они были реализованы в Idris 0.9.14, и я успешно использовал induction для некоторых доказательств. Однако они работают только для некоторых типов библиотек; в то время как, например, Vect поддерживает их, почти изоморфный All - нет:

-Main.h2> induction ys1 INTERNAL ERROR: induction needs an eliminator for Data.Vect.Quantifiers.All
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

К сожалению, документации по языку не так много, и я не смог найти, как реализовать анализ исключений/вариантов для пользовательских типов. Копаясь в Prelude, я нашел модификатор %elim, но это не помогло. Может ли кто-нибудь привести пример, скажем, для вышеупомянутого All?


algebraic-data-types idris formal-verification
person Yuuri    schedule 11.12.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Тактика induction может использоваться только для типов, которые были объявлены с помощью %elim. Некоторые люди считают, что Идрис должен автоматически генерировать элиминаторы, когда это возможно, но с этим могут быть некоторые технические трудности.

Может ли кто-нибудь привести пример, скажем, для вышеупомянутого All?

Насколько я могу судить, не должно возникнуть проблем с добавлением %elim к определению All (просто отредактируйте файл Quantifiers.idr и перекомпилируйте idris). Вы можете отправить запрос на вытягивание на Github.

person jch    schedule 17.12.2014
comment
Спасибо! Когда я пытался добавить %elim (к моему пользовательскому типу), сначала это не сработало, но теперь это сработало. Наверное, пришлось что-то обновить или перекомпилировать. - person Yuuri; 25.12.2014