, 명령`가져 오기 BigN` 8.6 COQ 사용했다하지만 COQ에

8.7 내가 COQ 8.6 COQ 8.7 I와 라이브러리하지만 수입 코드 Require Import BigN.으로의 bignum에게, 명령`가져 오기 BigN` 8.6 COQ 사용했다하지만 COQ에

$ opam upgrade bignum 
Already up-to-date.

를 설치하는 OPAM을 사용 필요 오류가 발생합니다. 그래서이 코드 줄을 bignum_problem.v 파일에서 분리했습니다. 그런 다음 coqc bignum_problem을 실행하는 COQ 모듈에 대한 문서가 나는 파일 BigN.vo이 필요하지만, 그런 파일이 .opam 디렉토리에 나타납니다 제안 응답

File "./bignum_problem.v", line 1, characters 15-19:

Error: Unable to locate library BigN .

을 생산하고 있습니다. 내가 뭘 놓치고 있니?

출처

2017-10-30 Barry Jay

bignum은 OCaml 라이브러리를 가리키는 것으로 보입니다. 대신 coq-bignums을 설치하는 것이 좋습니다. 방금 컴퓨터에 라이브러리를 설치 했으므로 명령을 사용하여 BigN을 요청할 수있었습니다.

From Bignums Require Import BigN.

출처

2017-10-30 03:21:06

감사합니다. 나는'http : // coq.io/opam/coq-bignums.8.7.0.html'을 발견하고 그들의 명령'opam install coq-bignums.8.7.0'을 시도했지만 여전히 오류가 발생합니다'[ERROR] No package named coq-bignums가 발견되었습니다. " –

@ BarryJay'opam install coq-bignums.8.7.0'을 통해 설치할 수있었습니다. 라이브러리를 설치하기 전에'opam update'를 실행해야합니다. –

또한 coq 관련 repo가 필요합니다. 'opam repo add coq-released https : // coq.inria.fr/opam/released' – gallais

, 명령`가져 오기 BigN` 8.6 COQ 사용했다하지만 COQ에

답변

관련 문제