Require loads the library, while Import displays its definitions in scope. Require Import does both. If you download only the library, you will need to name the names fully qualified. Coq allows top-level modules corresponding to files to define modules; they must be imported separately to bring all their definitions to scope, and they cannot be Require d - what happens with ListNotations :
(* List is not loaded by default *) Fail Check List.map. (* 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.map. (* List.map = fun (AB : Type) (f : A -> B) => fix map (l : list A) : list B := match l with | nil => nil | (a :: t)%list => (fa :: map t)%list end : forall AB : 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.map. (* map = fun (AB : Type) (f : A -> B) => fix map (l : list A) : list B := match l with | [] => [] | a :: t => fa :: map t end : forall AB : Type, (A -> B) -> list A -> list B *)
Note that there are some quirks with how Coq handles modules, especially when compared to other languages:
- Coq does not require a full path to the module, only a unique suffix. Indeed, I rarely see complete import paths, even to standard library modules.
- Symbols cannot be used except by importing a module, and unlike most objects, there is no way to refer to a notation, completely or otherwise.
- Importing a module can have side effects, for example, changing the notation interpretation framework or settings if you use the
Global Set in the imported module. - Import is quite limited (especially compared to Haskell) - there is no way to rename a module during import or selectively import some definitions.