이드리스 사례/유도 전술

그들은 Idris 0.9.14에서 구현되었으며 어떤 증명을 위해 induction을 성공적으로 사용했습니다. 그러나 일부 라이브러리 유형에서만 작동합니다.이드리스 사례/유도 전술

-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

불행하게도 언어 문서의 많음이 아니다, 나는 사용자 정의 유형에 대한 제거/사례 분석을 구현하는 방법을 찾을 수 없습니다 : 예를 들어, Vect 그들을 지원하는 반면, All 거의-동형하지 않습니다. Prelude를 들여다 보니 %elim 수식어가 발견되었지만 도움이되지 않았습니다. 아무도 예를 들어 앞서 말한 All에 대한 예를들 수 있습니까?

출처

2014-12-11 Yuuri

induction 전술은 %elim으로 선언 된 유형에서만 사용할 수 있습니다. 어떤 사람들은 가능할 때마다 Idris가 자동으로 제거기를 생성해야한다고 생각하지만 기술적 인 어려움이있는 것으로 보입니다.

아무도 예를 들어 앞에서 말한 모든 것을 제공 할 수 있습니까?

는 지금까지 내가 말할 수있는, (그냥 파일 Quantifiers.idr을 편집하고 이드리스을 다시 컴파일) All의 정의에 %elim를 추가 아무 문제가 없어야합니다. Github에서 요청을 제출하고 싶을 수 있습니다.

출처

2014-12-17 20:22:11 jch

고마워요! 처음에 % elim을 (내 사용자 정의 유형에) 추가하려고 시도했지만 작동하지 않았지만 이제는 작동하지 않습니다. 아마도 뭔가를 업데이트하거나 다시 컴파일해야했습니다. – Yuuri

이드리스 사례/유도 전술

답변

관련 문제