Импорт довольно ограничен (особенно по сравнению с Haskell) - нет способа переименовать модуль во время импорта или выборочно импортировать некоторые определения.

какая разница между ...?

Требовать X.Импорт X.Требовать Импорт X.

Я в основном запомнил некоторые общие закономерности. Я обычно вижу код, используя Require Import X. Затем есть Import ListNotation. И я только что заметил, что можно написать только Require X. Какая разница? Некоторые практические примеры будут оценены.

 Anton Trunov18 мар. 2018 г., 18:17
Этот вопрос является дубликатомэтот.

Ответы на вопрос(1)

Решение Вопроса

Require загружает библиотеку, тогда какImport приносит свои определения в сферу.Require Import делает оба. Если у вас есть только загруженная библиотека, вам нужно обратиться к полностью квалифицированным именам. Coq позволяет модулям верхнего уровня, соответствующим файлам, определять модули; они должны быть импортированы отдельно, чтобы привести все их определения в область видимости, и они не могут бытьRequireд - вот что происходитListNotations:

(* List is not loaded by default *)
Fail Check List..

(* the full name is technically Coq.Lists.List *)
Require List.

(* note that lists are actually defined in Coq.Init.Datatypes which is 
imported by default, so [list] is  unqualified and the [x::xs] notation is 
already defined *)
Print List..
(*
List. =
fun (A B : Type) (f : A -> B) =>
fix  (l : list A) : list B :=
  match l with
  | nil => nil
  | (a :: t)%list => (f a ::  t)%list
  end
    : forall A B : Type, (A -> B) -> list A -> list B
*)

(* bring everything in List into scope *)
Import List.
(* this includes the ListNotations submodule *)
Import ListNotations.

(* note that now list notations are available, and the list notation scope is
open (from importing List) *)
Print List..
(*
 =
fun (A B : Type) (f : A -> B) =>
fix  (l : list A) : list B :=
  match l with
  | [] => []
  | a :: t => f a ::  t
  end
    : forall A B : Type, (A -> B) -> list A -> list B
*)

Обратите внимание на некоторые особенности работы Coq с модулями, особенно по сравнению с другими языками:

Coq не требует полного пути к модулю, только однозначный суффикс. На самом деле я редко вижу полные пути импорта, даже в стандартные библиотечные модули.Нотации нельзя использовать, кроме как путем импорта модуля, и, в отличие от большинства объектов, нет способа ссылаться на нотацию, полностью определенную или иным образом.Импорт модуля может иметь побочные эффекты, например, изменение областей интерпретации нотации или параметров настройки, если вы используетеGlobal Set в импортируемом модуле.Импорт довольно ограничен (особенно по сравнению с Haskell) - нет способа переименовать модуль во время импорта или выборочно импортировать некоторые определения.

Ваш ответ на вопрос