我目前正在与 velvm 合作，对其进行改造。我是一个coq新手。
这是原子实现： http ://www.cis.upenn.edu/~plclub/popl08-tutorial/code/coqdoc/Atom.html
例如，在 velvm 中，原子被用作 id 和标签。
我想在一个 llvm 转换中插入一段代码，为此我必须给出一个“原子”类型的标签。如何构建 Atom 标签？
把我的问题更笼统地说：1）为什么有人想使用Atom？2）我怎样才能建造一个？3）如果我以这种方式构造，考虑到原子在代码中的使用方式可能不同，我是否会遇到麻烦？
谢谢！
编辑： id 和标签的代码
Definition id := atom. (*r identities *)
Definition l := atom. (*r labels *)
查看您指向的文件（由 Chargueraud 和 Aydemir 提供），您了解 atom 类型用于表示您可以用来为事物命名的任何类型。
应该使用函数 atom_fresh_for_list 来创建一个新原子。这个函数的类型表明它不仅返回一个任意原子，而且还返回一些证明你得到的原子不存在于你作为参数提供的列表中。这就是你如何创建一个新的：你把所有旧的放在一个列表中，然后你调用函数 atom_fresh_for_list 并将它作为参数。结果，您获得了一个类型为 {x : atom | ...}。这不完全是一个原子：它是一个包含更多信息的原子。您可以通过以下方式获取原子：
让 (v, h) := atom_fresh_for_list ... 在 ...
然后，在第二个“...”中，变量 v 包含原子，您可以使用它。如果你需要证明这个原子是一个新原子，那么你可以使用另一个变量 h 来证明它。
伊夫
Yves 能够部分回答它，只是没有如何构造原子的示例。您需要使用 projT1。以下是此代码：
Definition an_atom : atom := (projT1 (atom_fresh_for_list nil)).
nil 是任何列表。