ssrnat는 Coq 8.7에 포함되어 있습니까?

Coq 8.7은 대중적인 Ssreflect 라이브러리를 통합합니다. 나는 그것이 Unable to locate library ssrnat with prefix Coq의 불평 ssrnat 가져올 때, 그러나ssrnat는 Coq 8.7에 포함되어 있습니까?

From Coq Require Import ssreflect ssrfun ssrbool.

, 그리고 나도 디스크에 COQ 분포 ssrnat을 찾을 수 없습니다 : 그 라이브러리는 따라서 다음과 같은 방식으로 가져올 수 있습니다. 어떤 이유로 든 ssrnat이 의도적으로 포함되지 않았습니까? 아니면 폴더가 다른 모듈에 포함되지 않았습니까? 아니면 설치에 문제가 있습니까?

출처

2017-12-16 LogicChains

'From mathcomp Import ssrnat가 필요합니다.'가 작동합니까? –

이렇게하면 "논리 경로 일치 접미사 <> 및 접두어 mathcomp에 바인딩 된 실제 경로를 찾을 수 없습니다." (저는 mathcomp를 설치하지 않았습니다.) – LogicChains

Coq Refman이'ssrnat'을 언급 했음에도 불구하고, 현재 표준 라이브러리에는 없다 (나의 설치는'$ HOME/.opam/4.06.0 /에'ssreflect','ssrfun','ssrbool' 만있다. lib/coq/plugins/ssr' 디렉토리). 그래서, 네, 당신은 mathcomp를 설치해야합니다. 덧붙여 말하면 [이 질문] (https://stackoverflow.com/questions/43955082/how-to-install-ssreflect-and-mathcomp-in-linux) 설치에 도움이 될 수 있습니다. –

ssrnat은 주 Coq 배포에 포함되지 않지만 언젠가 더 많은 라이브러리가 기본적으로 제공되는 확장 배포를 제공하기를 희망하지만.

Coq 8.7에는 전술 언어 자체 ssreflect과 몇 가지 기본 지원 라이브러리 ssrfun ssrbool이 포함되었습니다.

우리가 더 많이 포함하지 않은 이유는 ssrnat이 수학 - 계산 수학적 계층 구조를 사용하므로 더 "침입적인"변화이기 때문입니다.

플러그인이 포함되어있어 ssrnat을 설치하는 것이 매우 쉬운 작업입니다.

출처

2017-12-16 17:16:16 ejgallego

ssrnat는 Coq 8.7에 포함되어 있습니까?

답변

관련 문제