下载PDF摘要：文本编辑器代表作家使用的基本工具之一--软件开发人员、图书作者和数学家。文本编辑器必须按照预期工作，因为它允许用户完成他们的工作。我们将首先介绍一个成熟的文本编辑器的一个小子集--行编辑器。接下来，我们将给出一个完整文本编辑器的具体定义(规范)。然后，我们将在Coq中提供一个行编辑器的实现，然后我们将证明它是一个完整的文本编辑器。