Смущает импорт Coq

Может кто-нибудь, пожалуйста, сообщите мне о различиях между

  • Require Название.
  • Require Import Название.
  • Import Имя

?

1 ответ

  • Require: загрузить внешнюю библиотеку (обычно из стандартной библиотеки или папки user-contribs/);
  • Import: импортирует имена в модуле. Например, если у вас есть функция f в модуле M, выполнив Import M., вам нужно будет ввести f вместо M.f;
  • Require Import: выполняет как Require, так и Import.

licensed under cc by-sa 3.0 with attribution.