Некоторые из стандартной библиотеки Coq не могут быть загружены

Недавно я установил coq в свою систему (сначала из репозитория пользователя arch, но затем через opam, столкнувшись с той же проблемой). Когда я захотел попробовать стандартную библиотеку, я понял, что некоторые библиотеки могут быть загружены, а другие - нет. Например

Require Import Arith.
Require Import Logic.

отлично работает, тогда как

Require Import Lists.

или

Require Import Sets.

приводит к сообщению

Unable to locate library Lists.

Что может быть проблемой здесь?

coq,

0

Ответов: 0

Некоторые из стандартной библиотеки Coq не могут быть загружены

Недавно я установил coq в свою систему (сначала из репозитория пользователя arch, но затем через opam, столкнувшись с той же проблемой). Когда я захотел попробовать стандартную библиотеку, я понял, что некоторые библиотеки могут быть загружены, а другие - нет. Например

Require Import Arith.
Require Import Logic.

отлично работает, тогда как

Require Import Lists.

или

Require Import Sets.

приводит к сообщению

Unable to locate library Lists.

Что может быть проблемой здесь?

00Кок,
Похожие вопросы