需要，导入，需要导入 [英] Require, Import, Require Import

问题描述

在Coq中，...之间有什么区别?

In Coq, what's the difference between ... ?

• Require X.
• Import X.
• Require Import X.

• Require X.
• Import X.
• Require Import X.

我基本上已经记住了一些常见的模式.我通常使用Require Import X看到代码.然后是Import ListNotation.我只是注意到也可以只编写Require X.有什么不同?一些实际的例子将不胜感激.

I have basically memorized some common patterns. I usually see code using Require Import X. Then there's Import ListNotation. And I just noticed it's also possible to write just Require X. What's the difference? Some practical examples would be appreciated.

推荐答案

Require加载库，而Import将其定义引入范围. Require Import两者都做.如果仅加载了库，则需要引用完全限定的名称. Coq允许与文件相对应的顶级模块定义模块；这些必须分别导入才能将其所有定义引入范围，并且不能被Require d-ListNotations就是这样:

Require loads a library whereas Import brings its definitions into scope. Require Import does both. If you only have the library loaded, you'll need to refer to names fully qualified. Coq allows top-level modules corresponding to files to define modules; these have to be imported separately to bring all of their definitions into scope, and they can't be Required - that's what's going on 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 (A B : Type) (f : A -> B) =>
fix map (l : list A) : list B :=
  match l with
  | nil => nil
  | (a :: t)%list => (f a :: map 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.map.
(*
map =
fun (A B : Type) (f : A -> B) =>
fix map (l : list A) : list B :=
  match l with
  | [] => []
  | a :: t => f a :: map t
  end
    : forall A B : Type, (A -> B) -> list A -> list B
*)

请注意，关于Coq处理模块的方式有一些古怪之处，尤其是与其他语言相比:

Note there are some quirks with how Coq handles modules, especially compared to other languages:

• Coq不需要模块的完整路径，只需一个明确的后缀即可.实际上，我很少看到完整的导入路径，甚至没有标准库模块的导入路径.
• 除非导入模块，否则不能使用符号，并且与大多数对象不同，无法引用完全限定或其他形式的符号.
• 导入模块可能会有副作用，例如，如果在要导入的模块中使用Global Set，则更改符号解释范围或设置选项.
• 导入非常有限(尤其是与Haskell相比)-无法在导入时重命名模块或有选择地导入一些定义.

• Coq does not require a full path to a module, only an unambiguous suffix. Indeed I rarely see full import paths, even to standard library modules.
• Notations cannot be used except by importing the module, and unlike most objects there's no way to refer to a notation, fully qualified or otherwise.
• Importing a module can have side effects, for example changing notation interpretation scopes or setting options if you use Global Set in the module being imported.
• Importing is fairly limited (especially compared to Haskell) - there's no way to rename a module at import time, or selectively import some definitions.

这篇关于需要，导入，需要导入的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！